diff options
| author | GiteaBot <teabot@gitea.io> | 2021-12-05 00:25:15 +0000 |
|---|---|---|
| committer | GiteaBot <teabot@gitea.io> | 2021-12-05 00:25:15 +0000 |
| commit | 98d903a3c6060dd52e9301b3b965cb761cfd0789 (patch) | |
| tree | a21b05d3d62e1bf1b7b821d79ffca102081bd149 /options/gitignore/Idris | |
| parent | a1dca00974b8b179996fa52b28e627860179899c (diff) | |
| download | gitea-98d903a3c6060dd52e9301b3b965cb761cfd0789.tar.gz gitea-98d903a3c6060dd52e9301b3b965cb761cfd0789.zip | |
[skip ci] Updated licenses and gitignores
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 |