aboutsummaryrefslogtreecommitdiff
path: root/entries/funemy/.gitignore
diff options
context:
space:
mode:
authorfunemy2022-10-25 23:10:58 +0000
committerfunemy2022-10-25 23:10:58 +0000
commita92d2f2a96c36e758291d7150b4ff175ec2ec768 (patch)
treeddb1da2cbce7f450145c58d98271cbd90d3cb00b /entries/funemy/.gitignore
parent0a801e985fcb50d22acbe52a626d67d393c21851 (diff)
minor
Diffstat (limited to 'entries/funemy/.gitignore')
-rw-r--r--entries/funemy/.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/entries/funemy/.gitignore b/entries/funemy/.gitignore
index acb903a..3d2fbd5 100644
--- a/entries/funemy/.gitignore
+++ b/entries/funemy/.gitignore
@@ -1,3 +1,4 @@
.DS_Store
*.agdai
*.smt2
+**/.koka/*