update some settings; remove old pdf

fpvandoorn · Jan 9, 2025 · 93c2a5f · 93c2a5f
1 parent 77d4285
commit 93c2a5f
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 8 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,19 +1,11 @@
 {
     "files.exclude": {
-        ".devcontainer": true,
-        ".docker": true,
         "**/.DS_Store": true,
         "**/.DS_yml": true,
         "**/.git": true,
-        "**/.gitpod.yml": true,
-        "**/.vscode": true,
         "**/*.olean": true,
         "build": true,
         "html": true,
-        "lake-packages": true,
-        "lean-tactics.tex": true,
-        "LICENSE": true,
-        "mathematics_in_lean.pdf": true
     },
     "editor.minimap.enabled": false,
     "editor.acceptSuggestionOnEnter": "off",

diff --git a/lean-tactics.pdf b/lean-tactics.pdf