remove junk;
authorwenzelm
Wed, 04 Dec 2013 18:59:20 +0100
changeset 553164dd08fe126ba
parent 55315 391ba1e12360
child 55317 4300525448d7
child 56010 76211bc0e161
remove junk;
src/Tools/jEdit/lib/Tools/jedit
     1.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Wed Dec 04 18:38:26 2013 +0100
     1.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Dec 04 18:59:20 2013 +0100
     1.3 @@ -287,7 +287,7 @@
     1.4    cp "$ISABELLE_HOME/lib/logo/isabelle-32.gif" \
     1.5      "org/gjt/sp/jedit/icons/themes/tango/32x32/apps/isabelle.gif" || failed
     1.6    isabelle_jdk jar cfe jedit.jar org.gjt.sp.jedit.jEdit org || failed
     1.7 -  rm -rf org
     1.8 +  rm -rf META-INF org
     1.9    cd ..
    1.10  
    1.11    cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed