diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coqide.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml index 3b8696e9ba..775ab5b8c5 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -2480,7 +2480,7 @@ let main files = (fun () -> let av = Option.get ((get_current_view()).analyzed_view) in match av#filename with - | None -> () + | None -> warning "Call to external editor available only on named files" | Some f -> save_f (); let com = Flags.subst_command_placeholder !current.cmd_editor (Filename.quote f) in |