equal
deleted
inserted
replaced
88 [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME" |
88 [ "$SCALA_HOME/lib/scala-library.jar" ] || fail "Bad Scala directory: $SCALA_HOME" |
89 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/" |
89 cp "$SCALA_HOME/lib/scala-library.jar" "$JEDIT/jars/" |
90 |
90 |
91 cp -R "$THIS/dist-template/." "$JEDIT/." |
91 cp -R "$THIS/dist-template/." "$JEDIT/." |
92 |
92 |
93 cp Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" |
93 cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" |
94 cp lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" |
94 cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" |
95 cp lib/core-renderer.jar "$JEDIT/jars/" |
95 cp jars/lib/core-renderer.jar "$JEDIT/jars/" |
96 |
96 |
97 |
97 |
98 # build archive |
98 # build archive |
99 |
99 |
100 echo "${JEDIT}.tar.gz" |
100 echo "${JEDIT}.tar.gz" |