From cf9e8e0a4d224e2c542a22b170049f5b789a73e7 Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Tue, 27 Feb 2024 16:49:58 +0100 Subject: [PATCH] Remove unused ProB toolbar definition --- de.prob.plugin/fragment.xml | 13 ------------- 1 file changed, 13 deletions(-) diff --git a/de.prob.plugin/fragment.xml b/de.prob.plugin/fragment.xml index a6ecb8c3..96f3d639 100644 --- a/de.prob.plugin/fragment.xml +++ b/de.prob.plugin/fragment.xml @@ -10,17 +10,4 @@ name="ProB"> </perspective> </extension> - - <extension - point="org.eclipse.ui.menus"> - <menuContribution - locationURI="toolbar:org.eclipse.ui.main.toolbar"> - <toolbar - id="probtoolbar"> - </toolbar> - </menuContribution> - </extension> - - - </fragment> -- GitLab