diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-09 15:51:05 +0200 |
| commit | 8efb78da7900e7f13105aac8361272477f8f5119 (patch) | |
| tree | 6efe7fbf8c847b6e17239aebb7283ff125024def /ide | |
| parent | 3c481b2ef7e7abd813fdac22b4bbe8d89de88141 (diff) | |
| parent | 5ea2539d4a7d12938787a74a12112e76aaf2a4ee (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/ide_slave.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index 6a386e050..79affb36f 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -383,8 +383,6 @@ 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, _ = |