Make .gitignore temporarily visible in VSCode

fpvandoorn · Apr 30, 2024 · 4098df2 · 4098df2
1 parent 3605bca
commit 4098df2
Showing 1 changed file with 13 additions and 14 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,23 +1,22 @@
 {
     "files.exclude": {
-        "**/.git": true,
+        ".devcontainer": true,
+        ".docker": true,
         "**/.DS_Store": true,
-        "**/*.olean": true,
         "**/.DS_yml": true,
+        "**/.git": true,
         "**/.gitpod.yml": true,
         "**/.vscode": true,
-	".docker": true,
-	"build": true,
-	"html": true,
-	"lake-packages": true,
-	".gitignore": true,
-	"lake-manifest.json": true,
-	"lakefile.lean": true,
-	"lean-toolchain": true,
-	"mathematics_in_lean.pdf": true,
-    "LICENSE":true,
-    ".devcontainer":true,
-    "lean-tactics.tex":true
+        "**/*.olean": true,
+        "build": true,
+        "html": true,
+        "lake-manifest.json": true,
+        "lake-packages": true,
+        "lakefile.lean": true,
+        "lean-tactics.tex": true,
+        "lean-toolchain": true,
+        "LICENSE": true,
+        "mathematics_in_lean.pdf": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",