git.iko.soy/Idris-dev
on master help sign in
Consolidate reg069 into regression002
commit1e1c4496d539160934ee8377670911e899f88a74 authorSteven Shaw <steven@steshaw.org> dateFri 5 Aug 2016, 20:56 (10 years ago) parent2e20173
6 files changed+3−4
compare with master
unifiedsplit
test/reg069/expected−1 test/reg069/run−3 test/reg069/Mod.idr → test/regression002/Mod.idr test/regression002/expected+2 test/reg069/reg069.idr → test/regression002/reg069.idr test/regression002/run+1
test/reg069/expecteddeleted−1
@@ -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
118118 Did you mean to refer to Main.nat?
119119reg068.idr:2:6:When checking constructor Main.ze:
120120Type 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 <<!
2727:load reg055a.idr
2828:load reg056.idr
2929:load reg068.idr
30+:load reg069.idr
3031!
3132
3233rm -f *.ibc