aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-17 15:24:15 +0200
committerEmilio Jesus Gallego Arias2018-10-23 00:42:04 +0200
commit1db19a8f454e0f8c5a60101c87ccd38e0883d530 (patch)
tree5b575feb0118a20aa027ebcce2b5028ccfd142cf /Makefile
parent2d714ebc0ea9588b4346249a574d9eda63dd389d (diff)
[build] Refactoring to config lib and ocamldebug tweaks.
We make `config` into a properly library. This is more uniform and useful for some clients. This also matches what was done in Dune. Next step would be to push dependencies on `Coq_config` upwards, only the actual toplevel binaries should depend on it. We also remove the stale `camlp5.dbg` and refactor the dbg files a bit, isolating the bits that are specific to the plugin / lib building method used by makefile.
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index b74e4e5d4f..9ac32625ab 100644
--- a/Makefile
+++ b/Makefile
@@ -261,7 +261,7 @@ cacheclean:
find theories plugins test-suite -name '.*.aux' -exec rm -f {} +
cleanconfig:
- rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq dev/camlp5.dbg config/Info-*.plist
+ rm -f config/Makefile config/coq_config.ml dev/ocamldebug-coq config/Info-*.plist
distclean: clean cleanconfig cacheclean timingclean