From e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 8 May 2018 00:52:33 +0200 Subject: [toplevel] Don't ignore output filename provided by user in -o This was a silly bug introduced in 675a1dc401eb9a5540ba5bc9a522c1f84d4c3d54 that forgot to properly forward the command line option. Thanks to @SkySkimmer for finding out the problem. closes #7447 --- toplevel/coqtop.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'toplevel') diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 38351a377..809490166 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 -- cgit v1.2.3