equal
deleted
inserted
replaced
72 JEDIT="jedit-${VERSION}" |
72 JEDIT="jedit-${VERSION}" |
73 |
73 |
74 rm -rf "$JEDIT" jedit |
74 rm -rf "$JEDIT" jedit |
75 mkdir "$JEDIT" |
75 mkdir "$JEDIT" |
76 |
76 |
|
77 rm -f jedit && ln -s "$JEDIT" jedit |
|
78 |
77 |
79 |
78 # copy stuff |
80 # copy stuff |
79 |
81 |
80 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
82 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
81 cp -R "$JEDIT_HOME/." "$JEDIT/." |
83 cp -R "$JEDIT_HOME/." "$JEDIT/." |