summaryrefslogtreecommitdiff
path: root/backends/lean/.gitignore
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/.gitignore2
1 files changed, 2 insertions, 0 deletions
diff --git a/backends/lean/.gitignore b/backends/lean/.gitignore
new file mode 100644
index 00000000..6aef0860
--- /dev/null
+++ b/backends/lean/.gitignore
@@ -0,0 +1,2 @@
+lake-packages/
+build/ \ No newline at end of file