chore: add lakefile.olean to .gitignore

leanprover-community / quote4

Intuitive, type-safe expression quotations for Lean 4.

Apache License 2.0

75 stars 12 forks source link

chore: add lakefile.olean to .gitignore #25

Closed kim-em closed 12 months ago

kim-em commented 12 months ago

When we compile quote4 as a dependency, the lakefile.olean gets created, and then pollutes output from tools that watch git repositories (e.g. in VSCode we see the lake-package/Qq/lakefile.olean showing up when viewing Mathlib).

digama0 commented 12 months ago

you should probably unwatch lake-packages altogether though, for the reported issue.