Merge branch 'newtree'

[Faustine.git] / .gitignore

diff --git a/.gitignore b/.gitignore
index 93730f51560faa205da6dad75bdaeed8b024bb0e..bb12dc2ad92b1afff69233dbfa6c956396477122 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -5,3 +5,9 @@ gmon.out
 ouput_sounds/output* # default names
 /Makefile # only in the current directory, because Makefile.in is sufficient
 *.svg
+*.cm[iox]
+*~
+parser.ml
+lexer.ml
+*.mli
+.depend*