From 1d570e9c3c848bad0dec4410f116256349873b14 Mon Sep 17 00:00:00 2001
From: Jan Midtgaard <mail@janmidtgaard.dk>
Date: Tue, 6 Aug 2024 11:01:18 +0200
Subject: [PATCH] Reduce repetition count to 100

---
 dune | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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)))))