Re #7065: Remove .vscode/settings.json from version control again

agda · Feb 13, 2024 · a6b8648 · a6b8648
1 parent 2816d75
commit a6b8648
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 26 deletions.
diff --git a/.gitignore b/.gitignore
@@ -24,6 +24,7 @@
 .stack-work-*/
 .stack-work/
 .sw[a-p]
+.vscode/settings.json
 .\#*
 /benchmark/Create/hs-import-*
 /benchmark/Create/import-*

diff --git a/.vscode/settings.json b/.vscode/settings.json