diff options
Diffstat (limited to 'ide/ide_slave.ml')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 59d9078bb..62e1bad43 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -345,6 +345,8 @@ let init = match file with | None -> Stm.get_current_state () | Some file -> + if not (Filename.check_suffix file ".v") then + error "A file with suffix .v is expected."; let dir = Filename.dirname file in let open Loadpath in let open CUnix in let initial_id, _ = |