Add .gitignore for generated files
This commit is contained in:
parent
c19f00d714
commit
72a3203891
|
@ -0,0 +1,13 @@
|
||||||
|
*.cmi
|
||||||
|
*.cmo
|
||||||
|
*.cma
|
||||||
|
*.cmx
|
||||||
|
*.cmxa
|
||||||
|
*.top
|
||||||
|
*.o
|
||||||
|
*.a
|
||||||
|
._bcdi/
|
||||||
|
._ncdi/
|
||||||
|
._d/
|
||||||
|
cpdf
|
||||||
|
*.annot
|
Loading…
Reference in New Issue