ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-21 22:17:19 +03:00
Code Issues Projects Releases Wiki Activity

adjust tests with --consolewidth for use with -f curses

Browse Source
This commit is contained in:
Andreas Reuleaux 2015-03-19 17:24:36 +00:00
parent 8ab6beac57
commit 6bac17b37d
3 changed files with 10 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
test/reg056/run
View File

@ -1,3 +1,3 @@
#!/usr/bin/env bash
idris $@ reg056.idr -o reg056
idris --consolewidth 80 $@ reg056.idr -o reg056
rm -f *.ibc

9
test/totality001/expected
View File

@ -1,3 +1,6 @@
test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad
test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad
test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad
test010.idr:15:1:
Main.foo is possibly not total due to: Main.MkBad
test010a.idr:9:1:
main.bar is possibly not total due to: main.MkBad
test010b.idr:9:1:
main.bar is possibly not total due to: main.MkBad

6
test/totality001/run
View File

@ -1,6 +1,6 @@
#!/usr/bin/env bash
idris $@ --check test010.idr
idris $@ --check test010a.idr
idris $@ --check test010b.idr
idris --consolewidth 80 $@ --check test010.idr
idris --consolewidth 80 $@ --check test010a.idr
idris --consolewidth 80 $@ --check test010b.idr
rm -f *.ibc