diff options
| author | Emilio Jesus Gallego Arias | 2018-11-09 18:57:10 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-09 18:57:10 +0100 |
| commit | 7e3c54c09bdd748e2e2a60a94891b65481776041 (patch) | |
| tree | 8635c000d2d5f67b12b9058a3fc6d6c9579d1db3 | |
| parent | 1761f8ed41f3891f8b6edc0dd256cd18e47a74fb (diff) | |
| parent | c5213ab2a33087286a7ef224b8d2c73f8d19176d (diff) | |
Merge PR #8956: Fix dune runtest invocation
| -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 |