git.iko.soy/Idris-dev
on master help sign in
Consolidate reg006 into regression002
c318c38Steven Shaw
test/reg006/expecteddeleted−2
compare with master
unifiedsplit
@@ -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:
4No such variable EvenList
4No such variable EvenList
5reg003a.idr:9:6:When checking type of Main.test:
5reg003a.idr:9:6:When checking type of Main.test:
6No such variable EvenList
6No 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 @@
3${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
3${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
4:load reg003.idr
4:load reg003.idr
5:load reg003a.idr
5:load reg003a.idr
6+:load reg006.idr
6!
7!
7
8
8rm -f *.ibc
9rm -f *.ibc