mirror of
https://github.com/github/gitignore.git
synced 2026-08-25 17:32:47 +02:00
Merge pull request #4818 from vicgeentor/patch-1
Update Agda.gitignore to exclude MAlonzo directories in any location
This commit is contained in:
commit
f963896e65
@ -1,2 +1,2 @@
|
||||
*.agdai
|
||||
MAlonzo/**
|
||||
**/MAlonzo/**
|
||||
|
||||
Loading…
Reference in New Issue
Block a user