git.iko.soy/Idris-dev
on master help sign in
Move `timeout` from `test/bin/` to `test/scripts/`
276ba0aSteven Shaw
test/basic010/run+1−1
compare with master
unifiedsplit
@@ -2,7 +2,7 @@
2
2
3set -eu
3set -eu
4
4
5−TIMEOUT=../bin/timeout
5+TIMEOUT=../scripts/timeout
6
6
7$TIMEOUT 10 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010
7$TIMEOUT 10 "${IDRIS:-idris}" "$@" Main.idr --nocolour --check --warnreach -o basic010
8$TIMEOUT 5 ./basic010
8$TIMEOUT 5 ./basic010
test/reg039/run+1−1
@@ -2,6 +2,6 @@
2
2
3set -eu
3set -eu
4
4
5−TIMEOUT=../bin/timeout
5+TIMEOUT=../scripts/timeout
6
6
7$TIMEOUT 60 "${IDRIS:-idris}" "$@" --nocolour reg039.idr --exec go
7$TIMEOUT 60 "${IDRIS:-idris}" "$@" --nocolour reg039.idr --exec go
test/bin/timeout → test/scripts/timeoutrenamed

The content is the same.