aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2011-04-26 12:51:19 +0000
committerletouzey2011-04-26 12:51:19 +0000
commitfd7494fe50e85c01c92b7fc47a089afae9df5dd5 (patch)
tree0a6cadcbcd9e595466654db040f718bbae549a17
parent18c9de9f7ad965d514c9f77e36e6607418131f6f (diff)
Coqide: fix remove_current_view_page (#2499)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14065 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--ide/coqide.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d6ebdc307c..915cd0603b 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -290,7 +290,8 @@ let remove_current_view_page () =
session_notebook#remove_page c
in
let current = session_notebook#current_term in
- if current.script#buffer#modified then
+ if not current.script#buffer#modified then do_remove ()
+ else
match GToolbox.question_box ~title:"Close"
~buttons:["Save Buffer and Close";
"Close without Saving";