Merge 0e5d7be211 into f963896e65

mirror of https://github.com/github/gitignore.git synced 2026-08-30 11:47:22 +02:00
2026-08-30 11:47:22 +02:00 · 2026-04-03 14:24:57 -07:00
1 changed files with 0 additions and 2 deletions
--- a/Lean.gitignore
+++ b/Lean.gitignore
@ -1,2 +0,0 @@
 # cache and other artifacts produced by Lean's Lake build tool
 .lake/
		`@ -1,2 +0,0 @@`
			`# cache and other artifacts produced by Lean's Lake build tool`
			`.lake/`