From 6b0199b638da7bdc648fa4e53c94544d9c5b57cb Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Wed, 18 Apr 2012 19:24:01 +0000
Subject: Fixed the CoqIDE preference width

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15217 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/preferences.ml         | 2 +-
 ide/utils/configwin.ml     | 4 ++--
 ide/utils/configwin_ihm.ml | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/ide/preferences.ml b/ide/preferences.ml
index eb63b14897..d320dddab4 100644
--- a/ide/preferences.ml
+++ b/ide/preferences.ml
@@ -694,7 +694,7 @@ let configure ?(apply=(fun () -> ())) () =
 (*
   Format.printf "before edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
-  let x = edit ~apply ~width:640 "Customizations" cmds in
+  let x = edit ~apply "Customizations" cmds in
 (*
   Format.printf "after edit: current.text_font = %s@." (Pango.Font.to_string !current.text_font);
 *)
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 3ff607991e..4606ef29fd 100644
--- a/ide/utils/configwin.ml
+++ b/ide/utils/configwin.ml
@@ -60,9 +60,9 @@ let html = Configwin_ihm.html
 
 let edit
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400)
+    title ?width ?height
     conf_struct_list =
-  Configwin_ihm.edit ~with_apply: true ~apply title ~width ~height conf_struct_list
+  Configwin_ihm.edit ~with_apply: true ~apply title ?width ?height conf_struct_list
 
 let get = Configwin_ihm.edit ~with_apply: false ~apply: (fun () -> ())
 
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index c13a0b3cf4..7dbd04529e 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -1136,12 +1136,12 @@ let tabbed_box conf_struct_list buttons tooltips =
    to configure the various parameters. *)
 let edit ?(with_apply=true)
     ?(apply=(fun () -> ()))
-    title ?(width=400) ?(height=400)
+    title ?width ?height
     conf_struct =
   let dialog = GWindow.dialog
     ~position:`CENTER
     ~modal: true ~title: title
-    ~height ~width
+    ?height ?width
     ()
   in
   let tooltips = GData.tooltips () in
-- 
cgit v1.2.3