diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-27 18:28:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-09-27 18:28:48 +0200 |
| commit | 72c1fefcfb3f0dff02005034685f6b58ff84b3cc (patch) | |
| tree | b3618351d80a7519d75c65d198445be572ae0391 /ide/coqide.ml | |
| parent | e8b9ee76af721c32b2d5cfcdae4ecbf47b341545 (diff) | |
Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.
Diffstat (limited to 'ide/coqide.ml')
| -rw-r--r-- | ide/coqide.ml | 1 |
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 |