aboutsummaryrefslogtreecommitdiff
path: root/.gitignore
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 /.gitignore
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 '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 0 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore
index 538124b8e5..709e87cc9c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -55,7 +55,6 @@ config/coq_config.ml
config/coq_config.py
config/Info-*.plist
dev/ocamldebug-coq
-dev/camlp5.dbg
plugins/micromega/csdpcert
plugins/micromega/.micromega.ml.generated
kernel/byterun/dllcoqrun.so