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 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile') diff --git a/Makefile b/Makefile index 0078dba20..2637996ed 100644 --- a/Makefile +++ b/Makefile @@ -87,7 +87,7 @@ EXISTINGMLI := $(call find, '*.mli') ## Files that will be generated GENML4FILES:= $(ML4FILES:.ml4=.ml) -export GENMLFILES:=$(LEXFILES:.mll=.ml) tools/tolink.ml kernel/copcodes.ml +export GENMLFILES:=$(LEXFILES:.mll=.ml) kernel/copcodes.ml export GENHFILES:=kernel/byterun/coq_jumptbl.h export GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -- cgit v1.2.3