diff options
| author | Gaëtan Gilbert | 2018-12-17 14:51:31 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-17 14:51:31 +0100 |
| commit | 76d64fc2df0ddeb08e5ef0661ceee9fdba1da3b1 (patch) | |
| tree | 162792d1ba0b8c1a7a6396fc1e2042d4243aded6 /test-suite/dune | |
| parent | 854d3e1b404fb3ee9087ffb07cbba7cc9196c1f9 (diff) | |
| parent | 85b91b71abe7e60a9096ae31b9d0b4afda2189bb (diff) | |
Merge PR #8856: [gitlab] Test Ocaml trunk.
Diffstat (limited to 'test-suite/dune')
| -rw-r--r-- | test-suite/dune | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/dune b/test-suite/dune index c5fa0bb14a..eae072553a 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -70,4 +70,4 @@ (progn ; XXX: we will allow to set the NJOBS variable in a future Dune ; version, either by using an env var or by letting Dune set `-j` - (run make -j 2 BIN= PRINT_LOGS=1)))) + (run make -j 2 BIN= PRINT_LOGS=1 UNIT_TESTS=%{env:COQ_UNIT_TEST=unit-tests})))) |