clarified names (again), e.g. relevant for "Plugin Options";
authorwenzelm
Fri, 23 Jul 2021 10:32:34 +0200
changeset 74052 f34d54b0e5de
parent 74051 bd575b1bd9bf
child 74053 54a11c37d5bc
clarified names (again), e.g. relevant for "Plugin Options";
src/Tools/jEdit/jedit_main/plugin.props
--- a/src/Tools/jEdit/jedit_main/plugin.props	Thu Jul 22 13:07:09 2021 +0200
+++ b/src/Tools/jEdit/jedit_main/plugin.props	Fri Jul 23 10:32:34 2021 +0200
@@ -3,7 +3,7 @@
 ##:wrap=soft:maxLineLen=100:
 
 #identification
-plugin.isabelle.jedit_main.Plugin.name=Isabelle Main
+plugin.isabelle.jedit_main.Plugin.name=Isabelle
 plugin.isabelle.jedit_main.Plugin.author=Johannes H\u00F6lzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
 plugin.isabelle.jedit_main.Plugin.version=11.2
 plugin.isabelle.jedit_main.Plugin.description=Isabelle/jEdit main plugin