mirror of
https://github.com/ilyakooo0/Idris-dev.git
synced 2024-09-21 14:09:30 +03:00
adjust test totality007 with --consolewidth for use with -f curses
This commit is contained in:
parent
694bdf64d8
commit
343e956085
@ -1,3 +1,4 @@
|
||||
Type checking ./Totality.idr
|
||||
Totality.idr:4:1:Totality.foo is not total as there are missing cases
|
||||
Totality.idr:4:1:
|
||||
Totality.foo is not total as there are missing cases
|
||||
Totality.idr:4:1:Could not build: Totality.foo is not total as there are missing cases
|
||||
|
@ -2,6 +2,6 @@ package totality
|
||||
|
||||
-- totality007
|
||||
-- Test that the package builder doesn't allow totality errors in a build
|
||||
opts = ""
|
||||
opts = "--consolewidth 80"
|
||||
sourcedir = src
|
||||
modules = Totality
|
||||
|
Loading…
Reference in New Issue
Block a user