add cmi files
This commit is contained in:
parent
fea7eb431c
commit
f179ae0dfb
1 changed files with 1 additions and 0 deletions
|
@ -23,3 +23,4 @@ ignore = Name *.nav
|
||||||
ignore = Name *.snm
|
ignore = Name *.snm
|
||||||
ignore = Name *.vrb
|
ignore = Name *.vrb
|
||||||
ignore = Name *.o
|
ignore = Name *.o
|
||||||
|
ignore = Name *.cmi
|
||||||
|
|
Loading…
Reference in a new issue