# HG changeset patch
# User wenzelm
# Date 1386178706 -3600
# Node ID 391ba1e12360a707bc7a461dc2bb23e59171f67b
# Parent  617ddc60f914169160ce1c97410b55488f22a633
recover main entry point from d9c88171b393 -- occasionally useful with plain "java -jar jedit.jar";

diff -r 617ddc60f914 -r 391ba1e12360 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Dec 02 15:49:02 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Dec 04 18:38:26 2013 +0100
@@ -286,7 +286,7 @@
     "org/gjt/sp/jedit/icons/themes/classic/32x32/apps/isabelle.gif" || failed
   cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
     "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
-  isabelle_jdk jar cf jedit.jar org || failed
+  isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
   rm -rf org
   cd ..