diff options
| author | Guillaume Melquiond | 2017-01-13 08:40:17 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2017-01-13 08:40:17 +0100 |
| commit | aa21c209f85f37b3d16ff499bbeac15e967bf78f (patch) | |
| tree | c06142e64df545bfaeeaccce4b6c82d616d6f557 /ide | |
| 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.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 5b07d3ec3b..c0c4131ac5 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 |