chore(.gitignore): ignore lock files (#8368)

Two reasons: 1. Sometimes these accidentally make it into PRs (e.g. #8344) 2. Some editor plugins (like the git in vscode) update very frequently causing these files to appear and disappear quickly in the sidebar whenever lean compiles which is annoying
leanprover-community · Jul 19, 2021 · 739b353 · 739b353
1 parent ad7ab8d
commit 739b353
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/.gitignore b/.gitignore
@@ -8,3 +8,4 @@ all.lean
 /src/.noisy_files
 *~
 .DS_Store
+*.lock