projects / tatoo.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: ff22f9c)
Add generated files to the .gitignore.
authorKim Nguyễn <kn@lri.fr>
Tue, 23 Apr 2013 09:37:10 +0000 (11:37 +0200)
committerKim Nguyễn <kn@lri.fr>
Tue, 23 Apr 2013 09:37:10 +0000 (11:37 +0200)
.gitignore patch | blob | history

diff --git a/.gitignore b/.gitignore
index d7eda5a..804ed5a 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -14,3 +14,6 @@ autom4te.cache
 config.log
 remake
 .remake
 config.log
 remake
 .remake
+src/xpath/xpath_internal_parser.ml
+src/xpath/xpath_internal_parser.mli
+
Tree Automata TOOlkit