git.iko.soy/Idris-dev
on master help sign in
adjust test unique001 with --consolewidth for use with -f curses
7da6edaAndreas Reuleaux
test/unique001/expected+2−1
compare with master
unifiedsplit
@@ -17,4 +17,5 @@ with
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
17unique001b.idr:16:7:Borrowed name xs must not be used on RHS
18unique001c.idr:46:6:Unique name f is used more than once
18unique001c.idr:46:6:Unique name f is used more than once
19unique001d.idr:3:7:Borrowed name x must not be used on RHS
19unique001d.idr:3:7:Borrowed name x must not be used on RHS
20+unique001e.idr:3:10:
20−unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not
21+Constructor Main.Nil has a UniqueType, but the data type does not
test/unique001/run+7−6
@@ -1,9 +1,10 @@
1#!/usr/bin/env bash
1#!/usr/bin/env bash
2−idris $@ unique001.idr -o unique001
2+idris --consolewidth 80 $@ unique001.idr -o unique001
3./unique001
3./unique001
4−idris $@ unique001a.idr --check
4+idris --consolewidth 80 $@ unique001a.idr --check
5−idris $@ unique001b.idr --check
5+idris --consolewidth 80 $@ unique001b.idr --check
6−idris $@ unique001c.idr --check
6+idris --consolewidth 80 $@ unique001c.idr --check
7−idris $@ unique001d.idr --check
7+idris --consolewidth 80 $@ unique001d.idr --check
8−idris $@ unique001e.idr --check
8+idris --consolewidth 80 $@ unique001e.idr --check
9rm -f unique001 *.ibc
9rm -f unique001 *.ibc
10+k