chore: update .gitignore

No longer needed. If you still have these directories around, just delete them.
dupuisf · Sep 3, 2024 · 1e0e2c3 · 1e0e2c3
1 parent 0a294fe
commit 1e0e2c3
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1 @@
-/build
-/lean_packages
 /.lake