Consolidate reg006 into regression002
commitc318c383d102eb5aa8a9ee5c57e688a78717f5d2
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:02 (10 years ago)
parent1db1851
test/reg006/expecteddeleted−2
@@ -1,2 +0,0 @@
1−reg006.idr:17:1:
2−RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
test/reg006/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg006.idr --check
3−rm -f *.ibc
test/regression002/expected+2
@@ -4,3 +4,5 @@ reg003a.idr:7:11:When checking type of Main.OCons:
44No such variable EvenList
55reg003a.idr:9:6:When checking type of Main.test:
66No such variable EvenList
7+reg006.idr:17:1:
8+RBTree.lookup is possibly not total due to recursive path RBTree.lookup --> RBTree.lookup
test/reg006/reg006.idr → test/regression002/reg006.idrrenamed
The content is the same.
test/regression002/run+1
@@ -3,6 +3,7 @@
33${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
44:load reg003.idr
55:load reg003a.idr
6+:load reg006.idr
67!
78
89rm -f *.ibc