summaryrefslogtreecommitdiffstats
path: root/options/gitignore/Idris
diff options
context:
space:
mode:
authorDaniel Baumann <daniel@debian.org>2024-10-18 20:33:49 +0200
committerDaniel Baumann <daniel@debian.org>2024-10-18 20:33:49 +0200
commitdd136858f1ea40ad3c94191d647487fa4f31926c (patch)
tree58fec94a7b2a12510c9664b21793f1ed560c6518 /options/gitignore/Idris
parentInitial commit. (diff)
downloadforgejo-dd136858f1ea40ad3c94191d647487fa4f31926c.tar.xz
forgejo-dd136858f1ea40ad3c94191d647487fa4f31926c.zip
Adding upstream version 9.0.0.
Signed-off-by: Daniel Baumann <daniel@debian.org>
Diffstat (limited to 'options/gitignore/Idris')
-rw-r--r--options/gitignore/Idris7
1 files changed, 7 insertions, 0 deletions
diff --git a/options/gitignore/Idris b/options/gitignore/Idris
new file mode 100644
index 0000000..0f4e72c
--- /dev/null
+++ b/options/gitignore/Idris
@@ -0,0 +1,7 @@
+# Idris 2
+*.ttc
+*.ttm
+
+# Idris 1
+*.ibc
+*.o