aboutsummaryrefslogtreecommitdiff
path: root/Makefile.dune
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-08 15:01:24 +0100
committerGaëtan Gilbert2018-11-08 15:01:24 +0100
commita7522a0ea76a6efaed9342d08a95363b56d88d32 (patch)
tree9ab8bd176949a072e0edb1f79502142cedcdb0b2 /Makefile.dune
parent108c15b51a7d5f647c8681fe7a37c86f0c5a8b9c (diff)
Remove checker printers
Now that the checker is using the regular kernel files it can also use the normal printers.
Diffstat (limited to 'Makefile.dune')
-rw-r--r--Makefile.dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune
index d201d1783a..11a31b174d 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -42,7 +42,7 @@ check: voboot
COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc
PLUGIN_FILES=$(wildcard plugins/*/*.mlpack)
-PRINTER_FILES=dev/top_printers.cma dev/checker_printers.cma
+PRINTER_FILES=dev/top_printers.cma
QUICKBYTE_TARGETS=$(COQTOP_FILES) $(PLUGIN_FILES:.mlpack=.cma) $(PRINTER_FILES) topbin/coqtop_byte_bin.bc
QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxa) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe