first-commit
This commit is contained in:
7
options/gitignore/Idris
Normal file
7
options/gitignore/Idris
Normal file
@@ -0,0 +1,7 @@
|
||||
# Idris 2
|
||||
*.ttc
|
||||
*.ttm
|
||||
|
||||
# Idris 1
|
||||
*.ibc
|
||||
*.o
|
Reference in New Issue
Block a user