From b9ad512a45f4fb82510c9edaf7ca0f6eac30744f Mon Sep 17 00:00:00 2001
From: Ananth Venkatesh <ananth@functor.systems>
Date: Sat, 28 Mar 2026 21:42:41 -0700
Subject: [PATCH 1/2] feat: create Lean.gitignore

---
 Lean.gitignore | 2 ++
 1 file changed, 2 insertions(+)
 create mode 100644 Lean.gitignore

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

From 5f760225cf9ccac8ee884ff303e87127d9673679 Mon Sep 17 00:00:00 2001
From: Ananth Venkatesh <ananth@functor.systems>
Date: Fri, 3 Apr 2026 20:04:27 -0400
Subject: [PATCH 2/2] fix: only match on `.lake` directory

Co-authored-by: Devin Dooley <dooleydevin@github.com>
---
 Lean.gitignore | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Lean.gitignore b/Lean.gitignore
index f4361862..d4aa2921 100644
--- a/Lean.gitignore
+++ b/Lean.gitignore
@@ -1,2 +1,2 @@
 # cache and other artifacts produced by Lean's Lake build tool
-.lake
+.lake/