src/Tools/jEdit/makedist
changeset 34478 095e5cae6656
parent 34469 bd813e4e97d3
child 34512 14d70378f1c7
equal deleted inserted replaced
34475:f963335dbc6b 34478:095e5cae6656
    82 
    82 
    83 # copy stuff
    83 # copy stuff
    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" "$JEDIT/build-support"
    88 
    88 
    89 mkdir -p "$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/"