git.iko.soy/Idris-dev
on 372d2ea help sign in
Idris-dev/test/basic010/run
41 lines 1.1 kB history raw
1#!/usr/bin/env bash
4declare -a extraargs
5for arg in "$@"
6do
7 extraargs=("${extraargs[@]}" "'$arg'")
8done
10if (which timeout&>/dev/null); then
11 timeout 10 idris $@ Main.idr --nocolour --check --warnreach -o basic010
12 timeout 5 ./basic010
13else
14 # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
15 # Here copied from reg039.
16 #
17 # Executes command with a timeout
18 # Params:
19 # $1 timeout in seconds
20 # $2 command
21 # Returns 1 if timed out 0 otherwise
22 timeout() {
24 time=$1
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 }"
32 if [ $? = 1 ] ; then
33 echo "Timeout after ${time} seconds"
34 fi
36 }
38 timeout 10 "idris ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
39 timeout 5 "./basic010"
40fi
41rm -f *.ibc basic010