[gui] make use of printer-tag in gui
Showing
- src/plugins/gui/design.ml 2 additions, 1 deletionsrc/plugins/gui/design.ml
- src/plugins/gui/history.ml 4 additions, 4 deletionssrc/plugins/gui/history.ml
- src/plugins/gui/pretty_source.ml 47 additions, 493 deletionssrc/plugins/gui/pretty_source.ml
- src/plugins/gui/pretty_source.mli 2 additions, 5 deletionssrc/plugins/gui/pretty_source.mli
- src/plugins/gui/property_navigator.ml 1 addition, 1 deletionsrc/plugins/gui/property_navigator.ml
- src/plugins/occurrence/register_gui.ml 1 addition, 1 deletionsrc/plugins/occurrence/register_gui.ml
- src/plugins/scope/dpds_gui.ml 2 additions, 1 deletionsrc/plugins/scope/dpds_gui.ml
- src/plugins/security_slicing/register_gui.ml 1 addition, 0 deletionssrc/plugins/security_slicing/register_gui.ml
- src/plugins/slicing/register_gui.ml 1 addition, 0 deletionssrc/plugins/slicing/register_gui.ml
- src/plugins/value/gui_files/register_gui.ml 2 additions, 1 deletionsrc/plugins/value/gui_files/register_gui.ml
- src/plugins/wp/GuiSource.ml 3 additions, 2 deletionssrc/plugins/wp/GuiSource.ml
Loading
Please register or sign in to comment