diff --git a/dune b/dune index f576681e0..37f6e8b6c 100644 --- a/dune +++ b/dune @@ -94,6 +94,6 @@ (write-file hoped "") (write-file failed-runs "") (run cmd /q /c - "for %G in (1,2,3,4, 5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") + "for %G in (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") ; edit the previous line to focus on a particular seed (diff failed-runs hoped)))))