test(tests/lean/bad_set_option): add tests for bad 'set_option' command
This commit is contained in:
parent
9d1e312c12
commit
36cfb7fac0
2 changed files with 5 additions and 0 deletions
3
tests/lean/bad_set_option.lean
Normal file
3
tests/lean/bad_set_option.lean
Normal file
|
@ -0,0 +1,3 @@
|
|||
set_option boo true
|
||||
|
||||
set_option pp.unicode a
|
2
tests/lean/bad_set_option.lean.expected.out
Normal file
2
tests/lean/bad_set_option.lean.expected.out
Normal file
|
@ -0,0 +1,2 @@
|
|||
bad_set_option.lean:1:11: error: unknown option 'boo', type 'help options.' for list of available options
|
||||
bad_set_option.lean:3:22: error: invalid Boolean option value, 'true' or 'false' expected
|
Loading…
Reference in a new issue