Commit 8ea8a38 1 parent db79e8a commit 8ea8a38 Copy full SHA for 8ea8a38
File tree 34 files changed +34
-34
lines changed
34 files changed +34
-34
lines changed Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolor delab001.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolor delab001.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolor docs001.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolor docs001.idr < input
3
3
rm * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --nobanner --nocolor --quiet docs002.idr < input
2
+ ${IDRIS:- idris} $@ --nobanner --nocolor --quiet --port none docs002.idr < input
3
3
rm * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolor docs003.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolor docs003.idr < input
3
3
rm * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolor docs004.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolor docs004.idr < input
3
3
rm * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolor docs005.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolor docs005.idr < input
3
3
rm * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
2
${IDRIS:- idris} $@ test001.idr -o test001
3
3
./test001
4
- ${IDRIS:- idris} $@ test001.idr --quiet < input
4
+ ${IDRIS:- idris} $@ test001.idr --quiet --port none < input
5
5
rm -f test001 test001.ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolour test022.idr --exec main
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolour test022.idr --exec main
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet test023.idr -o test023
2
+ ${IDRIS:- idris} $@ --quiet --port none test023.idr -o test023
3
3
rm -f test023 * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolour test024.idr --exec main < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolour test024.idr --exec main < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolour --check test026.idr
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolour --check test026.idr
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --nocolour --quiet Test.idr < input
2
+ ${IDRIS:- idris} $@ --nocolour --quiet --port none Test.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet test032.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none test032.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive002.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive002.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive003.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive003.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive004.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive004.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --nocolour --quiet interactive005.idr --consolewidth 70 < input
2
+ ${IDRIS:- idris} $@ --nocolour --quiet --port none interactive005.idr --consolewidth 70 < input
3
3
rm -f * .ibc
4
4
rm -f hello.bytecode
5
5
rm -f hello
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --port 5000 interactive006.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none --port 5000 interactive006.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ -p contrib --nobanner --nocolor < input | perl -pe ' s-Data\\Z-Data/Z-g'
2
+ ${IDRIS:- idris} $@ -p contrib --nobanner --nocolor --port none < input | perl -pe ' s-Data\\Z-Data/Z-g'
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --nobanner --nocolor < input
2
+ ${IDRIS:- idris} $@ --nobanner --nocolor --port none < input
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive009.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive009.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nobanner --nocolor < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nobanner --nocolor < input
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive011.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive011.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --nocolour --consolewidth 70 --quiet interactive012.idr < input
2
+ ${IDRIS:- idris} $@ --nocolour --consolewidth 70 --quiet --port none interactive012.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet interactive013.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none interactive013.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet --nocolour --consolewidth 70 InterfaceName.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none -- nocolour --consolewidth 70 InterfaceName.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
2
3
- ${IDRIS:- idris} --nobanner --nocolour --quiet << !
3
+ ${IDRIS:- idris} --nobanner --nocolour --quiet --port none << !
4
4
:load layout001a.idr
5
5
:load layout001b.idr
6
6
:load layout001c.idr
Original file line number Diff line number Diff line change @@ -48,7 +48,7 @@ for T in "${TESTS[@]}"
48
48
do
49
49
echo ${T%% * } ${T##*# }
50
50
generate_testfile " tmptest.idr" " ${T%%#* } "
51
- ${IDRIS:- idris} $@ --quiet tmptest.idr -o tmptest || echo " missing primitive in ${CG} "
51
+ ${IDRIS:- idris} $@ --quiet --port none tmptest.idr -o tmptest || echo " missing primitive in ${CG} "
52
52
./tmptest <<< " ${T##*#}"
53
53
rm tmptest.idr tmptest.ibc tmptest
54
54
done
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --consolewidth 70 --quiet proof009.idr < input
2
+ ${IDRIS:- idris} $@ --consolewidth 70 --quiet --port none proof009.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --check --nocolour --quiet --consolewidth 70 quasiquote006.idr
2
+ ${IDRIS:- idris} $@ --check --nocolour --quiet --port none -- consolewidth 70 quasiquote006.idr
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet ott.idr -e example
2
+ ${IDRIS:- idris} $@ --quiet --port none ott.idr -e example
3
3
${IDRIS:- idris} $@ showu.idr -o reg040
4
4
./reg040
5
5
rm -f reg040 * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
- ${IDRIS:- idris} $@ --quiet reg075.idr < input
2
+ ${IDRIS:- idris} $@ --quiet --port none reg075.idr < input
3
3
rm -f * .ibc
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
2
3
- ${IDRIS:- idris} $@ --nobanner --nocolour --quiet << !
3
+ ${IDRIS:- idris} $@ --nobanner --nocolour --quiet --port none << !
4
4
:load reg003.idr
5
5
:load reg003a.idr
6
6
:load reg006.idr
Original file line number Diff line number Diff line change 1
1
#! /usr/bin/env bash
2
2
3
- ${IDRIS:- idris} --nobanner --nocolour --quiet << !
3
+ ${IDRIS:- idris} --nobanner --nocolour --quiet --port none << !
4
4
:load unique001a.idr
5
5
:load unique001b.idr
6
6
:load unique001c.idr
You can’t perform that action at this time.
0 commit comments