From 20d6c289bff303ec1a4cab3a56431989d0e527d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Sep 2016 21:59:38 +0200 Subject: 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 --- interp/dumpglob.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'interp/dumpglob.ml') 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' -- cgit v1.2.3