src/Tools/jEdit/makedist
changeset 34469 bd813e4e97d3
parent 34461 2dd8ced4f2ae
child 34478 095e5cae6656
equal deleted inserted replaced
34468:9d4b4f290676 34469:bd813e4e97d3
    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"
    89 mkdir -p "$JEDIT/jars"
    90 
    90 
    91 [ "$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"
    92 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
    92 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/"
    93 
    93 
    94 cp -R "$THIS/dist-template/." "$JEDIT/."
    94 cp -R "$THIS/dist-template/." "$JEDIT/."