Consolidate reg010 into regression002
commit812566d99dc81f7c6b7496cb36989238aa41216f
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:07 (10 years ago)
parent7701a90
test/reg010/expecteddeleted−3
@@ -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:
2121 1
2222 and
2323 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 <<!
55:load reg003a.idr
66:load reg006.idr
77:load reg007.lidr
8+:load reg010.idr
89!
910
1011rm -f *.ibc