git.iko.soy/Idris-dev
on master help sign in
Consolidate reg056 into regression002
e2f1da2Steven Shaw
test/reg056/expecteddeleted−2
compare with master
unifiedsplit
@@ -1,2 +0,0 @@
1−reg056.idr:7:7:dodgy n m Refl is a valid case
2−reg056.idr:10:6:nonk Refl is a valid case
test/reg056/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg056.idr -o reg056
3−rm -f *.ibc
test/regression002/expected+2
@@ -107,3 +107,5 @@ When checking an application of constructor Foo.CAny:
107 Attempting concrete match on polymorphic argument: Nothing
107 Attempting concrete match on polymorphic argument: Nothing
108reg055a.idr:13:7:When checking left hand side of Foo.apply:
108reg055a.idr:13:7:When checking left hand side of Foo.apply:
109Can't match on apply (\x => \y => x) a
109Can't match on apply (\x => \y => x) a
110+reg056.idr:7:7:dodgy n m Refl is a valid case
111+reg056.idr:10:6:nonk Refl is a valid case
test/reg056/reg056.idr → test/regression002/reg056.idrrenamed

The content is the same.

test/regression002/run+1
@@ -25,6 +25,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
25:load reg054.idr
25:load reg054.idr
26:load reg055.idr
26:load reg055.idr
27:load reg055a.idr
27:load reg055a.idr
28+:load reg056.idr
28!
29!
29
30
30rm -f *.ibc
31rm -f *.ibc