diff options
| author | Hugo Herbelin | 2014-12-07 14:02:59 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2014-12-07 15:20:31 +0100 |
| commit | 6736fb9db77be8a6f207b95ae0d5f7b3a843dc89 (patch) | |
| tree | 3046794d9942ab4b7a9cc0b596c32fea1630abcb /ide/coqide.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/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index ba20c771a6..c96a34018a 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1328,10 +1328,7 @@ let build_ui () = (** {2 Coqide main function } *) let make_file_buffer f = - let f = - if Sys.file_exists f || Filename.check_suffix f ".v" then f - else f^".v" - in + let f = if Filename.check_suffix f ".v" then f else f^".v" in FileAux.load_file ~maycreate:true f let make_scratch_buffer () = |