From ae1fed6bd9bbb175456f8f5ffc7ada0abc455896 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 2 Dec 2008 17:34:22 +0000
Subject: Miscellaneous fixes and improvements: - Fixed a virtual bug of
 unification (ever occurs if w_unify called with   a non-empty context of
 rel's, which is a priori uncommon). - Fixed Notation.out test. - Add better
 coqide error message in case editor is called on an unnamed file.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11650 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coqide.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ide')

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
-- 
cgit v1.2.3