equal
deleted
inserted
replaced
91 cp -R "$THIS/dist-template/." "$JEDIT/." |
91 cp -R "$THIS/dist-template/." "$JEDIT/." |
92 |
92 |
93 cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" |
93 cp jars/Isabelle-jEdit.jar "$JEDIT/jars/isabelle.jar" |
94 cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" |
94 cp jars/lib/Pure.jar "$JEDIT/jars/isabelle-Pure.jar" |
95 cp jars/lib/core-renderer.jar "$JEDIT/jars/" |
95 cp jars/lib/core-renderer.jar "$JEDIT/jars/" |
|
96 cp jars/lib/ErrorList.jar "$JEDIT/jars/" |
|
97 cp jars/lib/SideKick.jar "$JEDIT/jars/" |
96 |
98 |
97 |
99 |
98 # build archive |
100 # build archive |
99 |
101 |
100 echo "${JEDIT}.tar.gz" |
102 echo "${JEDIT}.tar.gz" |