From f5cb7eb3e68e4b7d1bb5eeb8d9c58666201945d4 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 10 Dec 2017 03:31:55 +0100
Subject: [make] remove unneeded generated file "tolink.ml"

When statically linking plugins, the "DECLARE PLUGIN" macro takes care
of properly setting up the loaded module table.

This setup was also done by `coqmktop`, thus in order to ease
bisecting, we didn't take care of it in the `coqmktop` deprecation.

Fixes #6364.
---
 Makefile.build | 18 ++++++------------
 1 file changed, 6 insertions(+), 12 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 3e4c5a0b4b..f11719c07b 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -386,12 +386,12 @@ $(COQTOP_BYTE_MLTOP): toplevel/coqtop_byte_bin.ml
 	$(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -package compiler-libs.toplevel -c $<
 
 ifeq ($(BEST),opt)
-$(COQTOPEXE): tools/tolink.cmx $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP)
+$(COQTOPEXE): $(LINKCMX) $(LIBCOQRUN) $(TOPLOOPCMA:.cma=.cmxs) $(COQTOP_OPT_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I vernac -I toplevel -I tools \
+	$(HIDE)$(OCAMLOPT) -linkall -linkpkg -I toplevel \
 	                   -I kernel/byterun/ -cclib -lcoqrun \
                            $(SYSMOD) -package camlp5.gramlib \
-	                   tools/tolink.cmx $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \
+	                   $(LINKCMX) $(OPTFLAGS) $(LINKMETADATA) \
 	                   $(COQTOP_OPT_MLTOP) toplevel/coqtop_bin.ml -o $@
 	$(STRIP) $@
 	$(CODESIGN) $@
@@ -401,20 +401,14 @@ $(COQTOPEXE): $(COQTOPBYTE)
 endif
 
 # Are "-cclib lcoqrun -dllib -lcoqrun" necessary?
-$(COQTOPBYTE): tools/tolink.cmo $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
+$(COQTOPBYTE): $(LINKCMO) $(LIBCOQRUN) $(TOPLOOPCMA) $(COQTOP_BYTE_MLTOP)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(OCAMLC) -linkall -linkpkg -I vernac -I toplevel -I tools \
+	$(HIDE)$(OCAMLC) -linkall -linkpkg -I toplevel \
 	                 -I kernel/byterun -dllpath $(abspath kernel/byterun) -cclib -lcoqrun -dllib -lcoqrun \
                          $(SYSMOD) -package camlp5.gramlib,compiler-libs.toplevel \
-	                 tools/tolink.cmo $(LINKCMO) $(BYTEFLAGS) \
+	                 $(LINKCMO) $(BYTEFLAGS) \
 	                 $(COQTOP_BYTE_MLTOP) toplevel/coqtop_bin.ml -o $@
 
-tools/tolink.ml: Makefile.build Makefile.common
-	$(SHOW)"ECHO... >" $@
-	$(HIDE)echo "let static_modules = \""$(STATICPLUGINS)"\"" > $@
-	$(HIDE)echo "let core_libs = \""$(LINKCMO)"\"" >> $@
-	$(HIDE)echo "let core_objs = \""$(OBJSMOD)"\"" >> $@
-
 # coqc
 
 COQCCMO:=lib/clib.cma lib/cErrors.cmo toplevel/usage.cmo tools/coqc.cmo
-- 
cgit v1.2.3