aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-12-02 08:36:00 +0000
committerGravatar glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-12-02 08:36:00 +0000
commit3e253de6854b139a8a1be76af2388ffa9a3dcdb2 (patch)
tree64862ea93c89b391c8f494211af62a8c2131b9b2 /.gitignore
parent3594d04da08dbeb58e29234dd33eaf6addc195d8 (diff)
Update .gitignore
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12554 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index 7bab0acb1..ba4811b8f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,6 +46,7 @@ dev/ocamlweb-doc/syntax.mli
ide/config_lexer.ml
ide/config_parser.ml
ide/config_parser.mli
+ide/coqLex.ml
ide/extract_index.ml
ide/find_phrase.ml
ide/highlight.ml