aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.dune2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.dune b/Makefile.dune
index fa59421983..2293c69c38 100644
--- a/Makefile.dune
+++ b/Makefile.dune
@@ -44,7 +44,7 @@ COQTOP_FILES=ide/idetop.bc ide/coqide_main.bc checker/coqchk.bc
PLUGIN_FILES=$(wildcard plugins/*/*.mlpack)
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
+QUICKOPT_TARGETS=$(COQTOP_FILES:.bc=.exe) $(PLUGIN_FILES:.mlpack=.cmxs) $(PRINTER_FILES:.cma=.cmxa) topbin/coqtop_bin.exe
quickbyte: voboot
dune build $(DUNEOPT) $(QUICKBYTE_TARGETS)