Consolidate unique003 into unique004
commite49367497fe7ef45afdfcbb06b64d9d3ab5d7542
authorSteven Shaw <steven@steshaw.org>
dateFri 5 Aug 2016, 22:35 (10 years ago)
parentc2113d7
test/unique003/expecteddeleted−4
@@ -1,4 +0,0 @@
1−unique003.idr:18:5:Type mismatch between
2− Int -> String
3−and
4− UniqueType (Int -> String)
test/unique003/rundeleted−3
@@ -1,3 +0,0 @@
1−#!/usr/bin/env bash
2−${IDRIS:-idris} $@ --nocolour unique003.idr --check
3−rm -f *.ibc
test/unique004/expected+4
@@ -20,3 +20,7 @@ unique002a.idr:15:5:Type mismatch between
2020 Int -> String
2121and
2222 UniqueType (Int -> String)
23+unique003.idr:18:5:Type mismatch between
24+ Int -> String
25+and
26+ UniqueType (Int -> String)
test/unique004/run+1
@@ -8,6 +8,7 @@ ${IDRIS:-idris} --nobanner --nocolour --quiet <<!
88:load unique001e.idr
99:load unique002.idr
1010:load unique002a.idr
11+:load unique003.idr
1112!
1213
1314rm -f *.ibc
test/unique003/unique003.idr → test/unique004/unique003.idrrenamed
The content is the same.