git.iko.soy/Idris-dev
on master help sign in
Consolidate reg069 into regression002
1e1c449Steven Shaw
test/reg069/expecteddeleted−1
compare with master
unifiedsplit
@@ -1 +0,0 @@
1−Mod.idr:11:1:public export Mod.natexp can't refer to export Mod.natfn
test/reg069/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg069.idr --check
3−rm -f *.ibc
test/reg069/Mod.idr → test/regression002/Mod.idrrenamed

The content is the same.

test/regression002/expected+2
@@ -118,3 +118,5 @@ reg068.idr:2:8-11:WARNING: nat is bound as an implicit
118 Did you mean to refer to Main.nat?
118 Did you mean to refer to Main.nat?
119reg068.idr:2:6:When checking constructor Main.ze:
119reg068.idr:2:6:When checking constructor Main.ze:
120Type level variable nat is not Main.nat
120Type level variable nat is not Main.nat
121+Mod.idr:11:1:
122+public export Mod.natexp can't refer to export Mod.natfn
test/reg069/reg069.idr → test/regression002/reg069.idrrenamed

The content is the same.

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