git.iko.soy/Idris-dev
on master help sign in
Consolidate reg010 into regression002
812566dSteven Shaw
test/reg010/expecteddeleted−3
compare with master
unifiedsplit
@@ -1,3 +0,0 @@
1−reg010.idr:5:15:
2−When checking left hand side of with block in usubst.unsafeSubst:
3−Can't match on with block in usubst.unsafeSubst warg a P x x px
test/reg010/rundeleted−2
@@ -1,2 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg010.idr --check --nocolour
test/regression002/expected+3
@@ -21,3 +21,6 @@ Specifically:
21 1
21 1
22 and
22 and
23 0
23 0
24+reg010.idr:5:15:
25+When checking left hand side of with block in usubst.unsafeSubst:
26+Can't match on with block in usubst.unsafeSubst warg a P x x px
test/reg010/reg010.idr → test/regression002/reg010.idrrenamed

The content is the same.

test/regression002/run+1
@@ -5,6 +5,7 @@ ${IDRIS:-idris} $@ --nobanner --nocolour --quiet <<!
5:load reg003a.idr
5:load reg003a.idr
6:load reg006.idr
6:load reg006.idr
7:load reg007.lidr
7:load reg007.lidr
8+:load reg010.idr
8!
9!
9
10
10rm -f *.ibc
11rm -f *.ibc