diff options
| author | Théo Zimmermann | 2020-05-12 15:09:37 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-05-13 12:27:00 +0200 |
| commit | 4c5e40b76960f798857919bb7d500aa5d86a424d (patch) | |
| tree | 02ef8e48376d37fa657dadf9db2e979b944506df | |
| parent | 684bbe55e9ee94f93486da6d2df97fcef3136d88 (diff) | |
Test interleaving of command-line options.
4 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/output/interleave_options_bad_order.out b/test-suite/output/interleave_options_bad_order.out new file mode 100644 index 0000000000..68dbaeb7b3 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.out @@ -0,0 +1,4 @@ +While loading initial state: +Warning: There is no flag or option with this name: "Extraction Optimize". +[unknown-option,option] +Extraction Optimize is on diff --git a/test-suite/output/interleave_options_bad_order.v b/test-suite/output/interleave_options_bad_order.v new file mode 100644 index 0000000000..9a70674b02 --- /dev/null +++ b/test-suite/output/interleave_options_bad_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-unset" "Extraction Optimize" "-ri" "Extraction") *) + +Test Extraction Optimize. diff --git a/test-suite/output/interleave_options_correct_order.out b/test-suite/output/interleave_options_correct_order.out new file mode 100644 index 0000000000..76bb2016eb --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.out @@ -0,0 +1 @@ +Extraction Optimize is off diff --git a/test-suite/output/interleave_options_correct_order.v b/test-suite/output/interleave_options_correct_order.v new file mode 100644 index 0000000000..7622d6ff52 --- /dev/null +++ b/test-suite/output/interleave_options_correct_order.v @@ -0,0 +1,3 @@ +(* coq-prog-args: ("-ri" "Extraction" "-unset" "Extraction Optimize") *) + +Test Extraction Optimize. |