This commit includes settings for Visual Studio Code, so that at least different people with the same editor (or me on multiple machines) get the same formatting. No functional changes.