Skip to content

Commit 8bd7e15

Browse files
committed
.byte are ignored
1 parent 0dced01 commit 8bd7e15

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

.gitignore

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ extraction/*.ml
22
extraction/*.mli
33
website/
44
_build/
5+
*.byte
56
*.native
67
*.annot
78
*.cmo

0 commit comments

Comments
 (0)