aboutsummaryrefslogtreecommitdiffhomepage
path: root/.gitignore
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-25 15:56:24 +0200
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-07-26 16:32:49 +0200
commit32be84c5ba384f93b350a551d7bbbeec03768046 (patch)
tree13f29c903bb30d6335af4e7162692ed65eb61d5a /.gitignore
parent41ef1ae0ad4043f308a06365f4e5b1369eb5d453 (diff)
No more dev/printers.cma
This file was only used during ocamldebug sessions (in the dev/db script). It was containing a large subset of the core cma files, up to the printing functions. There were a few notable exceptions, for instance no kernel/vm.cmo to avoid loading dllcoqrun.so in ocamldebug. But printers.cma was troublesome to maintain : almost each time an ML file was added/removed/renamed in the core of Coq, dev/printers.mllib had to be edited, in addition to the directory-specific .mllib (kernel/kernel.mllib and co). So I propose here to kill this file, and put instead in dev/db several "load_printer" of the core cma files. For that to work, we need to compile kernel/kernel.cma with the right -dllib and -dllpath options, but that shouldn't hurt (on the contrary). We also source now the camlpX cma in dev/db, via a new generated file dev/camlp4.dbg containing a load_printer of either gramlib.cma or camp4lib.cma. If one doesn't want to perform the whole "source db" at the start of an ocamldebug session, then the former "load_printer printers.cma" could be replaced by: source core.dbg load_printer top_printers.cmo See for instance the minimal dev/base_db.
Diffstat (limited to '.gitignore')
-rw-r--r--.gitignore1
1 files changed, 1 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore
index dd09fc53e..d91a674e1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -49,6 +49,7 @@ config/Makefile
config/coq_config.ml
config/Info-*.plist
dev/ocamldebug-coq
+dev/camlp4.dbg
plugins/micromega/csdpcert
kernel/byterun/dllcoqrun.so
coqdoc.sty