diff options
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index 88e49f2c11..8b735ec5a5 100644 --- a/.gitignore +++ b/.gitignore @@ -48,7 +48,7 @@ dev/ocamlweb-doc/syntax.mli ide/config_lexer.ml ide/config_parser.ml ide/config_parser.mli -ide/coqLex.ml +ide/coq_lex.ml ide/extract_index.ml ide/find_phrase.ml ide/highlight.ml |