diff options
| author | Enrico Tassi | 2018-11-12 19:49:56 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-11-12 19:49:56 +0100 |
| commit | fab415e89b864947ac878ccfd485229e9801ddf3 (patch) | |
| tree | 2e43456c7e086fb6c9d622feed7ae90e387a591c | |
| parent | 835ab6b50a4c3c0f7c4623bebf3c95f4fa49a79d (diff) | |
| parent | 09db499e23b0e47254c285f3ab51986e87e78641 (diff) | |
Merge PR #8960: [dune] Build `cmxs` files instead of `cmxa` in "quick" target.
| -rw-r--r-- | Makefile.dune | 2 |
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) |