Update vc and dev files

I merged your master into this branch before sending the pull request, otherwise github showed me an error message (which I did not quite understand, because the intermediate file changes seemed unrelated and actually could be merged without any conflicts in my local repository). Hope this does not cause similar problems as last time.