diff --git a/.gitignore b/.gitignore index 338ba3626f5b7..889a3819ca4e8 100644 --- a/.gitignore +++ b/.gitignore @@ -8,3 +8,4 @@ all.lean /src/.noisy_files *~ .DS_Store +*.lock