git.iko.soy/Idris-dev
on master help sign in
Consolidate reg035 into regression002
2683ffaSteven Shaw
test/reg035/expecteddeleted−1
compare with master
unifiedsplit
@@ -1 +0,0 @@
1−reg035b.idr:8:6:No such variable __pi_arg
test/reg035/rundeleted−5
@@ -1,5 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour --check reg035.idr
3−${IDRIS:-idris} $@ --nocolour --check reg035a.lidr
4−${IDRIS:-idris} $@ --nocolour --check reg035b.idr
5−rm -f *.ibc
test/regression002/expected+1
@@ -51,3 +51,4 @@ reg034.idr:6:5:When checking left hand side of bar:
51Can't match on bar xs xs Refl
51Can't match on bar xs xs Refl
52reg034.idr:9:5:When checking left hand side of foo:
52reg034.idr:9:5:When checking left hand side of foo:
53Can't match on foo f x x Refl
53Can't match on foo f x x Refl
54+reg035b.idr:8:6:No such variable __pi_arg
test/reg035/reg035.idr → test/regression002/reg035.idrrenamed

The content is the same.

test/reg035/reg035a.lidr → test/regression002/reg035a.lidrrenamed

The content is the same.

test/reg035/reg035b.idr → test/regression002/reg035b.idrrenamed

The content is the same.

test/regression002/run+3
@@ -14,6 +14,9 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
14:load reg028.idr
14:load reg028.idr
15:load reg028a.idr
15:load reg028a.idr
16:load reg034.idr
16:load reg034.idr
17+:load reg035.idr
18+:load reg035a.lidr
19+:load reg035b.idr
17!
20!
18
21
19rm -f *.ibc
22rm -f *.ibc