From aa21c209f85f37b3d16ff499bbeac15e967bf78f Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 13 Jan 2017 08:40:17 +0100
Subject: 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.
---
 ide/ide_slave.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'ide')

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
-- 
cgit v1.2.3