git.iko.soy/Idris-dev
on master help sign in
adjust tests with --consolewidth for use with -f curses
commitd0a9beb12e86d4a2a7fb969f85df437d5754cc86 authorAndreas Reuleaux <arx@a-rx.info> dateThu 19 Mar 2015, 14:42 (12 years ago) parent73da7d4
6 files changed+19−13
compare with master
unifiedsplit
test/reg007/run+1−1 test/reg010/expected+2−1 test/reg010/run+1−1 test/reg018/expected+10−5 test/reg018/run+4−4 test/reg023/run+1−1
test/reg007/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris --nocolour --check $@ reg007.lidr
2+idris --consolewidth 80 --nocolour --check $@ reg007.lidr
33rm -f *.ibc
test/reg010/expected+2−1
@@ -1,2 +1,3 @@
1−reg010.idr:5:15:When elaborating left hand side of with block in usubst.unsafeSubst:
1+reg010.idr:5:15:
2+When elaborating left hand side of with block in usubst.unsafeSubst:
23Can't match on with block in usubst.unsafeSubst warg a P x x px
test/reg010/run+1−1
@@ -1,2 +1,2 @@
11#!/usr/bin/env bash
2−idris $@ reg010.idr --check --nocolour
2+idris --consolewidth 80 $@ reg010.idr --check --nocolour
test/reg018/expected+10−5
@@ -1,5 +1,10 @@
1−reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat
2−reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat
3−reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB
4−reg018c.idr:21:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf
5−reg018d.idr:8:1:Main.pull is not total as there are missing cases
1+reg018a.idr:16:1:
2+conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat
3+reg018a.idr:21:1:
4+conat.loopForever is possibly not total due to: conat.minusCoNat
5+reg018b.idr:8:1:
6+A.showB is possibly not total due to recursive path A.showB
7+reg018c.idr:21:1:
8+CodataTest.inf is possibly not total due to: with block in CodataTest.inf
9+reg018d.idr:8:1:
10+Main.pull is not total as there are missing cases
test/reg018/run+4−4
@@ -1,6 +1,6 @@
11#!/usr/bin/env bash
2−idris $@ reg018a.idr --check
3−idris $@ reg018b.idr --check
4−idris $@ reg018c.idr --check
5−idris $@ reg018d.idr --check
2+idris --consolewidth 80 $@ reg018a.idr --check
3+idris --consolewidth 80 $@ reg018b.idr --check
4+idris --consolewidth 80 $@ reg018c.idr --check
5+idris --consolewidth 80 $@ reg018d.idr --check
66rm *.ibc
test/reg023/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris $@ reg023.idr --check
2+idris --consolewidth 80 $@ reg023.idr --check
33rm -f *.ibc