ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-11-13 07:26:59 +03:00
Code Issues Projects Releases Wiki Activity

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

Browse Source
This commit is contained in:
Andreas Reuleaux 2015-03-19 18:47:38 +00:00
parent 001fb4a34f
commit 2a7d6a96b9
2 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
test/totality008/expected
View File

@ -1 +1,2 @@
totality008.idr:7:1:Main.ElimT is possibly not total due to: Main.c2
totality008.idr:7:1:
Main.ElimT is possibly not total due to: Main.c2

2
test/totality008/run
View File

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