diff --git a/dune b/dune index 7f801ff2..44a643d6 100644 --- a/dune +++ b/dune @@ -49,7 +49,7 @@ (write-file hoped "") (write-file failed-runs "") (bash - "for i in `seq 200`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") + "for i in `seq 100`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") ; edit the previous line to focus on a particular seed (diff failed-runs hoped)))))