diff options
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 d201d1783a..3d930cf47c 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -53,7 +53,7 @@ quickopt: voboot dune build $(DUNEOPT) $(QUICKOPT_TARGETS) test-suite: voboot - dune $(DUNEOPT) runtest + dune runtest $(DUNEOPT) release: voboot dune build $(DUNEOPT) -p coq |