[gui] use configure pattern for splitters
Showing
- src/plugins/gui/gtk_helper.ml 16 additions, 11 deletionssrc/plugins/gui/gtk_helper.ml
- src/plugins/gui/gtk_helper.mli 8 additions, 7 deletionssrc/plugins/gui/gtk_helper.mli
- src/plugins/gui/wbox.ml 19 additions, 10 deletionssrc/plugins/gui/wbox.ml
- src/plugins/gui/wbox.mli 9 additions, 3 deletionssrc/plugins/gui/wbox.mli
Loading
Please register or sign in to comment