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. --- .gitignore | 1 - 1 file changed, 1 deletion(-) (limited to '.gitignore') diff --git a/.gitignore b/.gitignore index 36536ec96..cec51986d 100644 --- a/.gitignore +++ b/.gitignore @@ -157,7 +157,6 @@ plugins/ssr/ssrvernac.ml kernel/byterun/coq_jumptbl.h kernel/copcodes.ml -tools/tolink.ml ide/index_urls.txt .lia.cache checker/names.ml -- cgit v1.2.3