diff options
| author | Emilio Jesus Gallego Arias | 2020-05-14 01:48:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-14 01:48:19 +0200 |
| commit | 734d73205097323f732fd218dcfb72a7355a77b3 (patch) | |
| tree | d20112b748288dd0f9f9d813c694f447cf2332f7 /test-suite | |
| parent | 8b0d7a14c114f438ca663301e6d275094692869b (diff) | |
| parent | 4c5e40b76960f798857919bb7d500aa5d86a424d (diff) | |
Merge PR #12097: Interleave commandline require/set/unset commands
Ack-by: Zimmi48
Reviewed-by: ejgallego
Diffstat (limited to 'test-suite')
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. |