diff options
| -rw-r--r-- | .gitignore | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 7bab0acb17..ba4811b8f8 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 |