diff options
Diffstat (limited to 'tools/memory-model/scripts/runlitmus.sh')
| -rwxr-xr-x | tools/memory-model/scripts/runlitmus.sh | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/memory-model/scripts/runlitmus.sh b/tools/memory-model/scripts/runlitmus.sh index c84124b32bee..62b47c7e1ba9 100755 --- a/tools/memory-model/scripts/runlitmus.sh +++ b/tools/memory-model/scripts/runlitmus.sh @@ -69,7 +69,7 @@ fi # Generate the assembly code and run herd7 on it. gen_theme7 -n 10 -map $mapfile -call Linux.call > $themefile -jingle7 -theme $themefile $litmus > $T/$hwlitmusfile 2> $T/$hwlitmusfile.jingle7.out -/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $T/$hwlitmusfile > $LKMM_DESTDIR/$hwlitmus.out 2>&1 +jingle7 -theme $themefile $litmus > $LKMM_DESTDIR/$hwlitmus 2> $T/$hwlitmusfile.jingle7.out +/usr/bin/time $LKMM_TIMEOUT_CMD herd7 -model $catfile $LKMM_DESTDIR/$hwlitmus > $LKMM_DESTDIR/$hwlitmus.out 2>&1 exit $? |