author | wenzelm |
Wed, 04 Dec 2013 18:59:20 +0100 | |
changeset 54667 | 4dd08fe126ba |
parent 54666 | 391ba1e12360 |
child 54668 | 76211bc0e161 |
--- 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