aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/wg_Command.ml
diff options
context:
space:
mode:
authorGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-22 09:22:12 +0000
committerGravatar gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-10-22 09:22:12 +0000
commitc93c937799c262e65d2c8cbaf3d9f7e60c590039 (patch)
tree4cc56818950c721597cad4ac64b785a92feeea60 /ide/wg_Command.ml
parent9269fe8688aa7ca1dfa40e9900987ea4713c7227 (diff)
Wg_Commands: when detached display the buffer name
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16901 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/wg_Command.ml')
-rw-r--r--ide/wg_Command.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/wg_Command.ml b/ide/wg_Command.ml
index 2a99d9c18..8755db372 100644
--- a/ide/wg_Command.ml
+++ b/ide/wg_Command.ml
@@ -84,7 +84,7 @@ let detachable ?title =
open Preferences
class command_window name coqtop =
- let frame = detachable ~title:"Query pane" () in
+ let frame = detachable ~title:(Printf.sprintf "Query pane (%s)" name) () in
let _ = frame#hide in
let _ = GtkData.AccelGroup.create () in
let notebook =