aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--ide/coqide.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/ide/coqide.ml b/ide/coqide.ml
index d1a799a77..450bfcdfb 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -937,7 +937,6 @@ let emit_to_focus window sgn =
let build_ui () =
let w = GWindow.window
~wm_class:"CoqIde" ~wm_name:"CoqIde"
- ~allow_grow:true ~allow_shrink:true
~width:window_width#get ~height:window_height#get
~title:"CoqIde" ()
in