From abd71630ca71fbf5f3eb457c6942a1a5e7c15cfc Mon Sep 17 00:00:00 2001 From: Sebastian Krings <sebastian@krin.gs> Date: Thu, 15 Jan 2015 12:08:48 +0100 Subject: [PATCH] fix warning --- de.prob.ui/plugin.xml | 32 -------------------------------- 1 file changed, 32 deletions(-) diff --git a/de.prob.ui/plugin.xml b/de.prob.ui/plugin.xml index 6bf2e1f2..d7fbd370 100644 --- a/de.prob.ui/plugin.xml +++ b/de.prob.ui/plugin.xml @@ -1041,22 +1041,6 @@ <separator name="de.prob.ui.separator2" visible="true"> - <visibleWhen> - <with - variable="selection"> - <iterate - operator="or"> - <or> - <instanceof - value="org.eventb.core.IMachineRoot"> - </instanceof> - <instanceof - value="org.eventb.core.IContextRoot"> - </instanceof> - </or> - </iterate> - </with> - </visibleWhen> </separator> <command commandId="de.prob.ui.starteventbanimation" @@ -1135,22 +1119,6 @@ <separator name="de.prob.ui.separator1" visible="true"> - <visibleWhen> - <with - variable="selection"> - <iterate - operator="or"> - <or> - <instanceof - value="org.eventb.core.IMachineRoot"> - </instanceof> - <instanceof - value="org.eventb.core.IContextRoot"> - </instanceof> - </or> - </iterate> - </with> - </visibleWhen> </separator> </menuContribution> <menuContribution -- GitLab