diff options
Diffstat (limited to 'tools/memory-model/scripts/runlitmus.sh')
| -rwxr-xr-x | tools/memory-model/scripts/runlitmus.sh | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index dfdb1f00fcc0..94608d4b6502 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -75,6 +75,6 @@ then cp $T/$hwlitmusfile.jingle7.out $LKMM_DESTDIR/$hwlitmus.err exit 253 fi -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -unroll 0 $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? |