diff options
| -rw-r--r-- | .gitignore | 14 |
1 files changed, 14 insertions, 0 deletions
@@ -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 |