Skip to content

Commit e8c56f7

Browse files
committed
Update gitignore.
1 parent bf45105 commit e8c56f7

File tree

1 file changed

+2
-0
lines changed

1 file changed

+2
-0
lines changed

.gitignore

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,5 @@
11
*.glob
22
*.vo
33
*.v.d
4+
*.ml
5+
*.mli

0 commit comments

Comments
 (0)