@@ -1,41 +1,10 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
4−declare -a extraargs
5+TIMEOUT=../scripts/timeout
7− extraargs=("${extraargs[@]}" "'$arg'")
10−if (which timeout&>/dev/null); then
11− timeout 10 ${IDRIS:-idris} $@ Main.idr --nocolour --check --warnreach -o basic010
7+$TIMEOUT 10 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010
12− timeout 5 ./basic010
8+$TIMEOUT 5 ./basic010
14− # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
15− # Here copied from reg039.
17− # Executes command with a timeout
19− # $1 timeout in seconds
21− # Returns 1 if timed out 0 otherwise
26− # start the command in a subshell to avoid problem with pipes
27− # (spawn accepts one command)
28− command="/bin/sh -c \"$2\""
30− expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }" | perl -pe 's/\r$//'
33− echo "Timeout after ${time} seconds"
38− timeout 10 "${IDRIS:-idris} ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
39− timeout 5 "./basic010"
41−rm -f *.ibc basic010
10+rm -f -- *.ibc basic010