src/Tools/jEdit/lib/Tools/jedit
changeset 55316 4dd08fe126ba
parent 55315 391ba1e12360
child 56018 6b2ca4850b71
     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