7da6eda · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

adjust test unique001 with --consolewidth for use with -f curses

commit7da6edae296ed488edc412bc69949c416ba4ad53 authorAndreas Reuleaux <arx@a-rx.info> dateThu 19 Mar 2015, 18:32 (12 years ago) parent343e956

2 files changed+9−7

unifiedsplit

test/unique001/expected+2−1

@@ -17,4 +17,5 @@ with

1717unique001b.idr:16:7:Borrowed name xs must not be used on RHS

1818unique001c.idr:46:6:Unique name f is used more than once

1919unique001d.idr:3:7:Borrowed name x must not be used on RHS

20−unique001e.idr:3:10:Constructor Main.Nil has a UniqueType, but the data type does not

20+unique001e.idr:3:10:

21+Constructor Main.Nil has a UniqueType, but the data type does not

test/unique001/run+7−6

@@ -1,9 +1,10 @@

11#!/usr/bin/env bash

2−idris $@ unique001.idr -o unique001

2+idris --consolewidth 80 $@ unique001.idr -o unique001

33./unique001

4−idris $@ unique001a.idr --check

5−idris $@ unique001b.idr --check

6−idris $@ unique001c.idr --check

7−idris $@ unique001d.idr --check

8−idris $@ unique001e.idr --check

4+idris --consolewidth 80 $@ unique001a.idr --check

5+idris --consolewidth 80 $@ unique001b.idr --check

6+idris --consolewidth 80 $@ unique001c.idr --check

7+idris --consolewidth 80 $@ unique001d.idr --check

8+idris --consolewidth 80 $@ unique001e.idr --check

99rm -f unique001 *.ibc

10+k