on 54e4e41 help sign in
35 lines 953 B history raw
1#!/usr/bin/env bash
4declare -a extraargs
5for arg in "$@"
6do
7 extraargs=("${extraargs[@]}" "'$arg'")
8done
9if (which timeout&>/dev/null); then
10 timeout 60 idris $@ --nocolour reg039.idr --exec go
11else
12 # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
13 # Executes command with a timeout
14 # Params:
15 # $1 timeout in seconds
16 # $2 command
17 # Returns 1 if timed out 0 otherwise
18 timeout() {
20 time=$1
22 # start the command in a subshell to avoid problem with pipes
23 # (spawn accepts one command)
24 command="/bin/sh -c \"$2\""
26 expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"
28 if [ $? = 1 ] ; then
29 echo "Timeout after ${time} seconds"
30 fi
32 }
33 timeout 60 "idris ${extraargs[*]} --nocolour reg039.idr --exec go"
34 fi
35 rm -f reg039 *.ibc