Merge pull request #79 from chabulhwi/ignore-backup-files

Ignore backup files
leanprover-community · Dec 30, 2024 · 301951e · 301951e
2 parents 66b27f3 + f9f1597
commit 301951e
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 15 deletions.
diff --git a/.gitignore b/.gitignore
@@ -3,3 +3,4 @@ lake-packages/
 .lake/
 **/.DS_Store
 .i18n/**/*.mo
+*~
diff --git a/vid_script.txt~ b/vid_script.txt~
-Original file line number
+Diff line change
@@ Expand Up / @@ -3,3 +3,4 @@ lake-packages/ @@
     .lake/
     **/.DS_Store
     .i18n/**/*.mo
+    *~