mirror of
https://github.com/github/gitignore.git
synced 2026-11-05 17:44:46 +01:00
Merge branch 'github:main' into patch-1
This commit is contained in:
commit
9b70f75462
2 files changed
+3
-1
No files matched your search
+1
-1
@@ -1,2 +1,2 @@
|
|||||||
*.agdai
|
*.agdai
|
||||||
MAlonzo/**
|
**/MAlonzo/**
|
||||||
@@ -0,0 +1,2 @@
|
|||||||
|
# cache and other artifacts produced by Lean's Lake build tool
|
||||||
|
.lake/
|
||||||
Reference in new issue
Block a user