diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 00:52:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-05-08 00:52:33 +0200 |
| commit | e9bd8cd805b7b350fe3a970e6be1c9ea2e88a1e8 (patch) | |
| tree | 1fb0a9ac511c8fe2b281f08ed6d915e38efd9a9f /toplevel | |
| parent | 6c8b00e47334f60f200256d45a5542fa80ce4b12 (diff) | |
[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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 5 |
1 files changed, 3 insertions, 2 deletions
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 |