Merge branch 'removal/gui/gtk2' into 'master'
[gui] remove GTK2 support Closes #1166 See merge request frama-c/frama-c!4111
No related branches found
No related tags found
Showing
- .gitignore 0 additions, 6 deletions.gitignore
- src/plugins/gui/GSourceView.2.ml 0 additions, 37 deletionssrc/plugins/gui/GSourceView.2.ml
- src/plugins/gui/GSourceView.2.mli 0 additions, 34 deletionssrc/plugins/gui/GSourceView.2.mli
- src/plugins/gui/GSourceView.ml 0 additions, 0 deletionssrc/plugins/gui/GSourceView.ml
- src/plugins/gui/GSourceView.mli 0 additions, 0 deletionssrc/plugins/gui/GSourceView.mli
- src/plugins/gui/debug_manager.ko.ml 0 additions, 23 deletionssrc/plugins/gui/debug_manager.ko.ml
- src/plugins/gui/debug_manager.mli 0 additions, 29 deletionssrc/plugins/gui/debug_manager.mli
- src/plugins/gui/debug_manager.ok.ml 0 additions, 79 deletionssrc/plugins/gui/debug_manager.ok.ml
- src/plugins/gui/design.ml 1 addition, 1 deletionsrc/plugins/gui/design.ml
- src/plugins/gui/dgraph_helper.mli 0 additions, 42 deletionssrc/plugins/gui/dgraph_helper.mli
- src/plugins/gui/dgraph_helper.no.ml 0 additions, 40 deletionssrc/plugins/gui/dgraph_helper.no.ml
- src/plugins/gui/dgraph_helper.yes.ml 0 additions, 60 deletionssrc/plugins/gui/dgraph_helper.yes.ml
- src/plugins/gui/dune 1 addition, 42 deletionssrc/plugins/gui/dune
- src/plugins/gui/gtk_compat.2.ml 0 additions, 74 deletionssrc/plugins/gui/gtk_compat.2.ml
- src/plugins/gui/gtk_compat.3.ml 0 additions, 47 deletionssrc/plugins/gui/gtk_compat.3.ml
- src/plugins/gui/gtk_compat.mli 0 additions, 49 deletionssrc/plugins/gui/gtk_compat.mli
- src/plugins/gui/menu_manager.ml 1 addition, 1 deletionsrc/plugins/gui/menu_manager.ml
- src/plugins/gui/property_navigator.ml 0 additions, 10 deletionssrc/plugins/gui/property_navigator.ml
- src/plugins/gui/wutil.ml 17 additions, 2 deletionssrc/plugins/gui/wutil.ml
- src/plugins/impact/gui/register_gui.ml 0 additions, 33 deletionssrc/plugins/impact/gui/register_gui.ml
Loading
Please register or sign in to comment