[gui] get rid of deprecated (and removed in gtk3) attributes allow_{shrink,grow}
Showing
- src/plugins/gui/debug_manager.ml 1 addition, 3 deletionssrc/plugins/gui/debug_manager.ml
- src/plugins/gui/design.ml 1 addition, 4 deletionssrc/plugins/gui/design.ml
- src/plugins/gui/gtk_helper.ml 2 additions, 2 deletionssrc/plugins/gui/gtk_helper.ml
- src/plugins/gui/launcher.ml 1 addition, 2 deletionssrc/plugins/gui/launcher.ml
- src/plugins/gui/wpane.ml 1 addition, 1 deletionsrc/plugins/gui/wpane.ml
- src/plugins/impact/register_gui.ml 1 addition, 3 deletionssrc/plugins/impact/register_gui.ml
Loading
Please register or sign in to comment