Skip to content

Commit 9421b1c

Browse files
committed
Ignore files generated by agda-mode
I'm not sure when agda-mode started to generate these files, or if this is a bug. Anyways, these can be safely ignored.
1 parent e435b32 commit 9421b1c

1 file changed

Lines changed: 3 additions & 0 deletions

File tree

.gitignore

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,9 @@
55
*.#*
66
.dir-locals.el
77

8+
# emacs' agda mode
9+
src/agda2-mode*
10+
811
# build
912
src/cc
1013
src/Main

0 commit comments

Comments
 (0)