diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 19:15:54 +0100 |
| commit | ce8e37b97ce9db6f39368c50fb0ee4a7839ce754 (patch) | |
| tree | a6678760bcd97cf004ba1f065352c8cad666bec3 /Makefile.dune | |
| parent | 7e3c54c09bdd748e2e2a60a94891b65481776041 (diff) | |
| parent | a7522a0ea76a6efaed9342d08a95363b56d88d32 (diff) | |
Merge PR #8949: Remove checker printers
Diffstat (limited to 'Makefile.dune')
| -rw-r--r-- | Makefile.dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune index 3d930cf47c..fa59421983 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 |