From 802366bdf00adf3849499f43ba07ee726da0668a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 19 May 2016 07:41:09 +0200 Subject: coqc: support -o option to specify output file name The -o option lets one put .vo or .vio files in a directory of choice, i.e. decouple the location of the sources and the compiled files. This ease the integration of Coq in already existing IDEs that handle the build process automatically (eg Eclipse) and also enables one to compile/run at the same time 2 versions of Coq on the same sources. Example: b.v depending on a.v coq8.6/bin/coqc -R out8.6 Test src/a.v -o out8.6/a.vo coq8.6/bin/coqc -R out8.6 Test src/b.v -o out8.6/b.vo coq8.7/bin/coqc -R out8.7 Test src/a.v -o out8.7/a.vo coq8.7/bin/coqc -R out8.7 Test src/b.v -o out8.7/b.vo --- lib/aux_file.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'lib/aux_file.ml') diff --git a/lib/aux_file.ml b/lib/aux_file.ml index f7bd81f85..c814438dd 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -25,9 +25,9 @@ let mk_absolute vfile = if Filename.is_relative vfile then CUnix.correct_path vfile (Sys.getcwd ()) else vfile -let start_aux_file_for vfile = - let vfile = mk_absolute vfile in - oc := Some (open_out (aux_file_name_for vfile)); +let start_aux_file ~aux_file:output_file ~v_file = + let vfile = mk_absolute v_file in + oc := Some (open_out output_file); Printf.fprintf (Option.get !oc) "COQAUX%d %s %s\n" version (Digest.to_hex (Digest.file vfile)) vfile -- cgit v1.2.3