From 4151b64d1f0a942c877d0994105074f8c18eb550 Mon Sep 17 00:00:00 2001 From: Michael Leuschel <leuschel@uni-duesseldorf.de> Date: Thu, 2 Apr 2020 09:48:21 +0200 Subject: [PATCH] change label of export POs menu command --- de.prob.eventb.disprover.ui/plugin.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/de.prob.eventb.disprover.ui/plugin.xml b/de.prob.eventb.disprover.ui/plugin.xml index 9d24e750..8b0ec03a 100644 --- a/de.prob.eventb.disprover.ui/plugin.xml +++ b/de.prob.eventb.disprover.ui/plugin.xml @@ -94,7 +94,7 @@ <command commandId="de.prob.eventb.disprover.ui.exportpos" icon="icons/prob_mini_logo.gif" - label="Export POs for ProB" + label="Export POs for ProB (probcli)" style="push"> </command> </menuContribution> -- GitLab