mathlib
739b353d - chore(.gitignore): ignore lock files (#8368)

Commit
4 years ago
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
Author
Parents
Loading