remove All.lean

loganrjmurphy · May 29, 2024 · 2628d91 · 2628d91
1 parent 766163e
commit 2628d91
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 1,388 deletions.
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+Book/All.lean
 /build
 /lake-packages/*
 /.lake/*