aboutsummaryrefslogtreecommitdiff
path: root/ide/utils
diff options
context:
space:
mode:
authorcoq2003-12-30 09:56:20 +0000
committercoq2003-12-30 09:56:20 +0000
commitb2c056c881dcb3035158ab177f2363c1527df397 (patch)
tree7e13f45a340cc82721a7ca4962ea4852d287157b /ide/utils
parenta08c4181d9580aeaf4d52a382a5c84a4040d5995 (diff)
ameliorations coqide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/utils')
-rw-r--r--ide/utils/configwin_ihm.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index b6f6550bd4..d359d3d706 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1039,6 +1039,7 @@ let edit ?(with_apply=true)
conf_struct_list =
let return = ref Return_cancel in
let window = GWindow.window
+ ~position:`CENTER
~modal: true ~title: title
~width: width ~height: height ()
in