diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-22 21:59:38 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2016-09-22 21:59:38 +0200 |
| commit | 20d6c289bff303ec1a4cab3a56431989d0e527d2 (patch) | |
| tree | 0a481eb21424fb747f3ebc4241e138b34d782be4 | |
| parent | 505ac480574d235cd2f40ca4b2debde0bb875146 (diff) | |
coqc -o now places .glob file near .vo file
All compilation (by)products are placed where -o specifies.
Used to be the case for .vo, .vio, .aux but not .glob
| -rw-r--r-- | interp/dumpglob.ml | 4 | ||||
| -rw-r--r-- | interp/dumpglob.mli | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 1e14eeb81..b020f8945 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -45,10 +45,10 @@ let dump_string s = if dump () && !glob_output != Feedback then Pervasives.output_string !glob_file s -let start_dump_glob vfile = +let start_dump_glob ~vfile ~vofile = match !glob_output with | MultFiles -> - open_glob_file (Filename.chop_extension vfile ^ ".glob"); + open_glob_file (Filename.chop_extension vofile ^ ".glob"); output_string !glob_file "DIGEST "; output_string !glob_file (Digest.to_hex (Digest.file vfile)); output_char !glob_file '\n' diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index a7c799114..e84a64052 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -9,7 +9,7 @@ val open_glob_file : string -> unit val close_glob_file : unit -> unit -val start_dump_glob : string -> unit +val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index de3d14483..55f3a31a3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -345,7 +345,7 @@ let compile verbosely f = Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); - Dumpglob.start_dump_glob long_f_dot_v; + Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in |