diff options
| -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" |