diff options
| author | Emilio Jesus Gallego Arias | 2018-07-04 16:48:01 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-11 01:28:43 +0200 |
| commit | dd25b08c3608b55dd9edb24304168efb56bc64c8 (patch) | |
| tree | 04f7a631e0b223a74958571b99cd7abaac2b1852 /Makefile.common | |
| 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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.common b/Makefile.common index fdaa94212a..727cb1e69b 100644 --- a/Makefile.common +++ b/Makefile.common @@ -89,6 +89,7 @@ INSTALLSH:=./install.sh MKDIR:=install -d CORESRCDIRS:=\ + coqpp \ config clib lib kernel kernel/byterun library \ engine pretyping interp proofs parsing printing \ tactics vernac stm toplevel |