diff options
Diffstat (limited to 'options/gitignore/Idris')
| -rw-r--r-- | options/gitignore/Idris | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/options/gitignore/Idris b/options/gitignore/Idris index c28bc7cc67..0f4e72c71c 100644 --- a/options/gitignore/Idris +++ b/options/gitignore/Idris @@ -1,2 +1,7 @@ +# Idris 2 +*.ttc +*.ttm + +# Idris 1 *.ibc *.o |