diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-13 08:40:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-01-13 08:40:17 +0100 |
| commit | aa21c209f85f37b3d16ff499bbeac15e967bf78f (patch) | |
| tree | c06142e64df545bfaeeaccce4b6c82d616d6f557 | |
| parent | 5391d15256af65a0ba0ead4ee6d1ec16f7e362cc (diff) | |
Fix broken .aux machinery.
Coq expects aux_file_name_for to give the aux file corresponding to the
input file whichever its Coq-related extension, be it .v or .vo or .vio.
Commit 3e6fa1c broke this contract when fixing bug #5183. As a
consequence, depending on the execution path, Coq would try to save or
load from either .foo.aux or .foo.vo.aux or .foo.vio.aux.
This commit reverts 3e6fa1c and fixes bug #5183 much earlier in the call
chain by not initializing hints when the input file does not end with .v.
This also restores 8.5 behavior with respect to aux file naming.
| -rw-r--r-- | ide/ide_slave.ml | 3 | ||||
| -rw-r--r-- | lib/aux_file.ml | 4 |
2 files changed, 2 insertions, 5 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5b07d3ec3..c0c4131ac 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -392,7 +392,8 @@ let init = Stm.add false ~ontop:(Stm.get_current_state ()) 0 (Printf.sprintf "Add LoadPath \"%s\". " dir) else Stm.get_current_state (), `NewTip in - Stm.set_compilation_hints file; + if Filename.check_suffix file ".v" then + Stm.set_compilation_hints file; Stm.finish (); initial_id end diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 0f0f09aa2..c6c7b4242 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -17,10 +17,6 @@ let version = 1 let oc = ref None -let chop_extension f = - if check_suffix f ".v" then chop_extension f - else f - let aux_file_name_for vfile = dirname vfile ^ "/." ^ chop_extension(basename vfile) ^ ".aux" |