diff options
| -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 |