diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 14:02:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-07 15:20:31 +0100 |
| commit | 6736fb9db77be8a6f207b95ae0d5f7b3a843dc89 (patch) | |
| tree | 3046794d9942ab4b7a9cc0b596c32fea1630abcb /ide/ide_slave.ml | |
| parent | 48509b6112fc857abdfc442c89821363043ac705 (diff) | |
Ensuring that ide_slave and stm receive only .v files from CoqIDE.
In particular, renouncing to original support for existing non .v
files in CoqIDE (hoping it is ok for anyone). Please amend if better
to propose.
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, _ = |