[gui] full upgrade to lablgtk3 beta
Showing
- src/plugins/gui/design.ml 2 additions, 2 deletionssrc/plugins/gui/design.ml
- src/plugins/gui/filetree.ml 2 additions, 4 deletionssrc/plugins/gui/filetree.ml
- src/plugins/gui/gtk_helper.ml 13 additions, 5 deletionssrc/plugins/gui/gtk_helper.ml
- src/plugins/gui/gtk_helper.mli 10 additions, 0 deletionssrc/plugins/gui/gtk_helper.mli
- src/plugins/gui/menu_manager.ml 7 additions, 16 deletionssrc/plugins/gui/menu_manager.ml
- src/plugins/gui/project_manager.ml 1 addition, 2 deletionssrc/plugins/gui/project_manager.ml
- src/plugins/gui/wfile.ml 3 additions, 3 deletionssrc/plugins/gui/wfile.ml
- src/plugins/gui/widget.ml 6 additions, 9 deletionssrc/plugins/gui/widget.ml
- src/plugins/metrics/register_gui.ml 5 additions, 10 deletionssrc/plugins/metrics/register_gui.ml
- src/plugins/scope/dpds_gui.ml 2 additions, 4 deletionssrc/plugins/scope/dpds_gui.ml
- src/plugins/slicing/register_gui.ml 1 addition, 2 deletionssrc/plugins/slicing/register_gui.ml
- src/plugins/studia/studia_gui.ml 3 additions, 5 deletionssrc/plugins/studia/studia_gui.ml
- src/plugins/value/gui_files/gui_callstacks_manager.ml 1 addition, 4 deletionssrc/plugins/value/gui_files/gui_callstacks_manager.ml
Loading
Please register or sign in to comment