aboutsummaryrefslogtreecommitdiff
path: root/config/config.mllib
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 /config/config.mllib
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 'config/config.mllib')
-rw-r--r--config/config.mllib1
1 files changed, 1 insertions, 0 deletions
diff --git a/config/config.mllib b/config/config.mllib
new file mode 100644
index 0000000000..ce3ddfca69
--- /dev/null
+++ b/config/config.mllib
@@ -0,0 +1 @@
+Coq_config