@@ -1,5 +1,35 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
3+# From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
4+# Here copied from reg039.
6+# Executes command with a timeout
8+# $1 timeout in seconds
10+# Returns 1 if timed out 0 otherwise
15+ # start the command in a subshell to avoid problem with pipes
16+ # (spawn accepts one command)
17+ command="/bin/sh -c \"$2\""
19+ expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
22+ echo "Timeout after ${time} seconds"
30+ extraargs=("${extraargs[@]}" "'$arg'")
3−idris $@ Main.idr --nocolour --check --warnreach -o basic010
33+timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
4−./basic010
34+timeout 5 "./basic010"
5rm -f *.ibc basic010
35rm -f *.ibc basic010