diff --git a/Lean.gitignore b/Lean.gitignore new file mode 100644 index 0000000000..f436186203 --- /dev/null +++ b/Lean.gitignore @@ -0,0 +1,2 @@ +# cache and other artifacts produced by Lean's Lake build tool +.lake