diff --git a/.gitignore b/.gitignore index c7d56e16dae..153f5f90bb0 100644 --- a/.gitignore +++ b/.gitignore @@ -2,11 +2,25 @@ *.x86 *.llvm *.out +*.cmx +*.dll *.exe *.orig *.cmo *.cmi *.d *.o +*.aux +*.cp +*.fn +*.ky +*.log +*.pdf +*.html +*.pg +*.toc +*.tp +*.vr .hg/ .hgignore +lexer.ml