Consolidate reg070 into regression002
commit5208aeb6e40d16eea37decbb0999cbf8607949c3
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 20:58 (10 years ago)
parent1e1c449
test/reg070/expecteddeleted−2
@@ -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:
120120Type level variable nat is not Main.nat
121121Mod.idr:11:1:
122122public 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 <<!
2828:load reg056.idr
2929:load reg068.idr
3030:load reg069.idr
31+:load reg070.idr
3132!
3233
3334rm -f *.ibc