diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-04 16:48:01 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 01:28:43 +0200 |
commit | dd25b08c3608b55dd9edb24304168efb56bc64c8 (patch) | |
tree | 04f7a631e0b223a74958571b99cd7abaac2b1852 /.gitignore | |
parent | d47ddf56bc93ae16280ce8a845a4b004fef52fb8 (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-- | .gitignore | 6 |
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 |