diff options
| author | Théo Zimmermann | 2018-05-11 10:38:58 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-05-11 10:38:58 +0200 |
| commit | 4abf92639c13002c2ca8aff0015a42aff5c6b329 (patch) | |
| tree | 77038f3e1e3d3a0ca01c458f51f5d32bbf7520b2 | |
| parent | 5da17b8c60846913db18b0f9216d63898933aa52 (diff) | |
| parent | 73e91542293af304ff25db9d3ea5495a9aa95249 (diff) | |
Merge PR #7456: [toplevel] Don't ignore output filename provided by user in -o
| -rwxr-xr-x | test-suite/misc/coqc_dash_o.sh | 15 | ||||
| -rw-r--r-- | test-suite/misc/coqc_dash_o.v | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 5 |
3 files changed, 19 insertions, 2 deletions
diff --git a/test-suite/misc/coqc_dash_o.sh b/test-suite/misc/coqc_dash_o.sh new file mode 100755 index 0000000000..f303214b9a --- /dev/null +++ b/test-suite/misc/coqc_dash_o.sh @@ -0,0 +1,15 @@ +#!/bin/bash + +DOUT=misc/tmp_coqc_dash_o/ +OUT=${DOUT}coqc_dash_o.vo + + +mkdir -p "${DOUT}" +rm -f "${OUT}" +$coqc misc/coqc_dash_o.v -o "${OUT}" +if [ ! -f "${OUT}" ]; then + printf "coqc -o not working" + exit 1 +fi +rm -fr "${DOUT}" +exit 0 diff --git a/test-suite/misc/coqc_dash_o.v b/test-suite/misc/coqc_dash_o.v new file mode 100644 index 0000000000..7426dff1a0 --- /dev/null +++ b/test-suite/misc/coqc_dash_o.v @@ -0,0 +1 @@ +Definition x := nat. diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 38351a377a..809490166c 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -315,11 +315,12 @@ let compile cur_feeder opts ~echo ~f_in ~f_out = CoqworkmgrApi.giveback 1 let compile_file cur_feeder opts (f_in, echo) = + let f_out = opts.compilation_output_name in if !Flags.beautify then Flags.with_option Flags.beautify_file - (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out:None) f_in + (fun f_in -> compile cur_feeder opts ~echo ~f_in ~f_out) f_in else - compile cur_feeder opts ~echo ~f_in ~f_out:None + compile cur_feeder opts ~echo ~f_in ~f_out let compile_files cur_feeder opts = let compile_list = List.rev opts.compile_list in |