aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-04 16:48:01 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-07-11 01:28:43 +0200
commitdd25b08c3608b55dd9edb24304168efb56bc64c8 (patch)
tree04f7a631e0b223a74958571b99cd7abaac2b1852 /.gitignore
parentd47ddf56bc93ae16280ce8a845a4b004fef52fb8 (diff)
[coqpp] Move to its own directory.
Coqpp has nothing to do with `grammar`, we thus place it in its own directory, which will prove convenient in more modular build systems. Note that we add `coqpp` to the list of global includes, we could have indeed added some extra rules, but IMHO not worth it as hopefully proper containment will be soon checked by Dune.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore6
1 files changed, 3 insertions, 3 deletions
diff --git a/.gitignore b/.gitignore
index 466f4c1a7..14ec71b93 100644
--- a/.gitignore
+++ b/.gitignore
@@ -115,7 +115,7 @@ dev/ocamldoc/*.css
# .mll files
-grammar/coqpp_lex.ml
+coqpp/coqpp_lex.ml
dev/ocamlweb-doc/lex.ml
ide/coq_lex.ml
ide/config_lexer.ml
@@ -128,8 +128,8 @@ ide/protocol/xml_lexer.ml
# .mly files
-grammar/coqpp_parse.ml
-grammar/coqpp_parse.mli
+coqpp/coqpp_parse.ml
+coqpp/coqpp_parse.mli
# .ml4 / .mlp files