.vscode/settings.json: add comment

sagemath · Aug 25, 2022 · 0938385 · 0938385
1 parent c5755d8
commit 0938385
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,4 +1,6 @@
 {
+    // This settings file is not ignored by git. It should be kept in sync with
+    // the trac repo.
     "python.defaultInterpreterPath": "./venv/bin/python3",
     "files.exclude": {
         "**/__pycache__": true,