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.

1 files changed, 6 insertions, 0 deletions

diff --git a/Makefile.build b/Makefile.build
index d5f9887b9..228b2e736 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -505,6 +505,12 @@ test-suite: world $(ALLSTDLIB).v
 # but the -include mechanism should already ensure that we have
 # up-to-date dependencies.
 
+# Specific rule for kernel.cma, with $(VMBYTEFLAGS).
+# This helps loading dllcoqrun.so during an ocamldebug
+kernel/kernel.cma: kernel/kernel.mllib
+	$(SHOW)'OCAMLC -a -o $@'
+	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) $(VMBYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)
+
 %.cma: %.mllib
 	$(SHOW)'OCAMLC -a -o $@'
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -a -o $@ $(filter-out %.mllib, $^)