diff --git a/dune b/dune index 25c50a71..b663fe49 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 -s 107236932 ; then echo $i >> failed-runs; fi; done") + "for i in `seq 100`; do echo Starting $i-th run; if ! ./focusedtest.exe -v -s 107236932 ; then echo $i >> failed-runs; fi; done") ; edit the previous line to focus on a particular seed (diff failed-runs hoped)))))