summaryrefslogtreecommitdiff
path: root/ide/utils/configwin.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:23:14 +0200
commit86535d84cc3cffeee1dcd8545343f234e7285530 (patch)
tree9b221c283c2971f7ac151397231059e1d239e723 /ide/utils/configwin.ml
parent39efc41237ec906226a3a53d7396d51173495204 (diff)
parent61dc740ed1c3780cccaec00d059a28f0d31d0052 (diff)
Diffstat (limited to 'ide/utils/configwin.ml')
-rw-r--r--ide/utils/configwin.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/utils/configwin.ml b/ide/utils/configwin.ml
index 3ff60799..4606ef29 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 () -> ())