diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:12 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 09:22:12 +0000 |
commit | c93c937799c262e65d2c8cbaf3d9f7e60c590039 (patch) | |
tree | 4cc56818950c721597cad4ac64b785a92feeea60 /ide/wg_Command.ml | |
parent | 9269fe8688aa7ca1dfa40e9900987ea4713c7227 (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.ml | 2 |
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 = |