aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:10:04 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-09-30 16:10:04 +0000
commit51798358c936ae3276a68d5045acb71023619cfb (patch)
treeaa35d16d165e374de8f44791a99a16a85ad64c12 /ide/coqide.ml
parentc96140256591d98b806a777e5e400f89f614a798 (diff)
CoqIDE: use #present to raise error window
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coqide.ml')
-rw-r--r--ide/coqide.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 165d7b080..0d32954ba 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1326,7 +1326,7 @@ let build_ui () =
let update_errwin () =
on_current_term (fun sn ->
fill_errwin (notebook#term_num (==) sn) sn.coqops#get_errors) in
- let _ = slaveinfobut#connect#clicked ~callback:errwin#misc#show in
+ let _ = slaveinfobut#connect#clicked ~callback:errwin#present in
let update sn =
let processed, to_process = sn.coqops#get_slaves_status in
let missing = to_process - processed in