# HG changeset patch
# User wenzelm
# Date 1386179960 -3600
# Node ID 4dd08fe126bad63aa05741d55fb3e86a2dbfc795
# Parent  391ba1e12360a707bc7a461dc2bb23e59171f67b
remove junk;

diff -r 391ba1e12360 -r 4dd08fe126ba src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Dec 04 18:38:26 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Dec 04 18:59:20 2013 +0100
@@ -287,7 +287,7 @@
   cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
     "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
   isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
-  rm -rf org
+  rm -rf META-INF org
   cd ..
 
   cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed