src/Tools/jEdit/makedist
changeset 34461 2dd8ced4f2ae
parent 34419 30e49efdd4e3
child 34469 bd813e4e97d3
equal deleted inserted replaced
34459:b08299e7bbe6 34461:2dd8ced4f2ae
    84 
    84 
    85 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
    85 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME"
    86 cp -R "$JEDIT_HOME/." "$JEDIT/."
    86 cp -R "$JEDIT_HOME/." "$JEDIT/."
    87 rm -rf "$JEDIT/jEdit"
    87 rm -rf "$JEDIT/jEdit"
    88 
    88 
       
    89 mkdir "$JEDIT/jars"
       
    90 
    89 [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
    91 [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME"
    90 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
    92 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
    91 
    93 
    92 cp -R "$THIS/dist-template/." "$JEDIT/."
    94 cp -R "$THIS/dist-template/." "$JEDIT/."
    93 
    95