diff options
| author | Pierre-Marie Pédrot | 2017-01-19 14:23:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-01-19 14:23:51 +0100 |
| commit | f22969902223ab54f56f25583b24dc27c4cd6f4e (patch) | |
| tree | 09c893b1dd14c9b2b38067a01486fc61452d0209 /ide | |
| parent | 34c19354c9997621a40ad053a2a12edcd8c5b5e4 (diff) | |
| parent | 8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (diff) | |
Merge branch 'v8.6'
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 48fd0a93e4..ae3dcd94a9 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -393,7 +393,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 |