idris-0.12.2: test/basic010/run

#!/usr/bin/env bash


declare -a extraargs
for arg in "$@"
do
    extraargs=("${extraargs[@]}" "'$arg'")
done

if (which timeout&>/dev/null); then
    timeout 10 ${IDRIS:-idris} $@ Main.idr --nocolour --check --warnreach -o basic010
    timeout 5  ./basic010
else
    # From http://unix.stackexchange.com/questions/43340/how-to-introduce-timeout-for-shell-scripting
    # Here copied from reg039.
    #
    # Executes command with a timeout
    # Params:
    #   $1 timeout in seconds
    #   $2 command
    # Returns 1 if timed out 0 otherwise
    timeout() {

        time=$1

        # start the command in a subshell to avoid problem with pipes
        # (spawn accepts one command)
        command="/bin/sh -c \"$2\""

        expect -c "set echo \"-noecho\"; set timeout $time; spawn -noecho $command; expect timeout { exit 1 } eof { exit 0 }"

        if [ $? = 1 ] ; then
            echo "Timeout after ${time} seconds"
        fi

    }

    timeout 10 "${IDRIS:-idris} ${extraargs[*]} Main.idr --nocolour --check --warnreach -o basic010"
    timeout 5  "./basic010"
fi
rm -f *.ibc basic010