git.iko.soy/Idris-dev
on master help sign in
Consolidate unique003 into unique004
e493674Steven Shaw
test/unique003/expecteddeleted−4
compare with master
unifiedsplit
@@ -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
20 Int -> String
20 Int -> String
21and
21and
22 UniqueType (Int -> String)
22 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 <<!
8:load unique001e.idr
8:load unique001e.idr
9:load unique002.idr
9:load unique002.idr
10:load unique002a.idr
10:load unique002a.idr
11+:load unique003.idr
11!
12!
12
13
13rm -f *.ibc
14rm -f *.ibc
test/unique003/unique003.idr → test/unique004/unique003.idrrenamed

The content is the same.