From 36cfb7fac0dc67f522ff8accb83473c90fc8a164 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 1 Feb 2015 20:20:35 -0800 Subject: [PATCH] test(tests/lean/bad_set_option): add tests for bad 'set_option' command --- tests/lean/bad_set_option.lean | 3 +++ tests/lean/bad_set_option.lean.expected.out | 2 ++ 2 files changed, 5 insertions(+) create mode 100644 tests/lean/bad_set_option.lean create mode 100644 tests/lean/bad_set_option.lean.expected.out diff --git a/tests/lean/bad_set_option.lean b/tests/lean/bad_set_option.lean new file mode 100644 index 000000000..b65e02362 --- /dev/null +++ b/tests/lean/bad_set_option.lean @@ -0,0 +1,3 @@ +set_option boo true + +set_option pp.unicode a diff --git a/tests/lean/bad_set_option.lean.expected.out b/tests/lean/bad_set_option.lean.expected.out new file mode 100644 index 000000000..78ce16f5d --- /dev/null +++ b/tests/lean/bad_set_option.lean.expected.out @@ -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