git.iko.soy/Idris-dev
on master help sign in
Consolidate reg070 into regression002
5208aebSteven Shaw
test/reg070/expecteddeleted−2
compare with master
unifiedsplit
@@ -1,2 +0,0 @@
1−reg070.idr:7:1:
2−Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
test/reg070/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ reg070.idr --check
3−rm -f *.ibc
test/regression002/expected+2
@@ -120,3 +120,5 @@ reg068.idr:2:6:When checking constructor Main.ze:
120Type level variable nat is not Main.nat
120Type level variable nat is not Main.nat
121Mod.idr:11:1:
121Mod.idr:11:1:
122public export Mod.natexp can't refer to export Mod.natfn
122public export Mod.natexp can't refer to export Mod.natfn
123+reg070.idr:7:1:
124+Test_show.Te implementation of Prelude.Show.Show is possibly not total due to: Prelude.Show.Test_show.Te implementation of Prelude.Show.Show, method show
test/reg070/reg070.idr → test/regression002/reg070.idrrenamed

The content is the same.

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