diff options
| author | Pierre-Marie Pédrot | 2016-09-27 18:28:48 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-27 18:28:48 +0200 |
| commit | 72c1fefcfb3f0dff02005034685f6b58ff84b3cc (patch) | |
| tree | b3618351d80a7519d75c65d198445be572ae0391 | |
| parent | e8b9ee76af721c32b2d5cfcdae4ecbf47b341545 (diff) | |
Fix bug #4553: CoqIDE gives warnings about deprecated GTK features.
| -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 d1a799a773..450bfcdfb1 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 |