equal
deleted
inserted
replaced
9 SUPER=$(cd "$THIS/.."; pwd) |
9 SUPER=$(cd "$THIS/.."; pwd) |
10 |
10 |
11 |
11 |
12 ## diagnostics |
12 ## diagnostics |
13 |
13 |
14 JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre17" |
14 JEDIT_HOME="" |
15 |
15 |
16 function usage() |
16 function usage() |
17 { |
17 { |
18 echo |
18 echo |
19 echo "Usage: $PRG [OPTIONS]" |
19 echo "Usage: $PRG [OPTIONS]" |
20 echo |
20 echo |
21 echo " Options are:" |
21 echo " Options are:" |
22 echo " -j DIR specify original jEdit distribution" |
22 echo " -j DIR specify original jEdit distribution" |
23 echo " (default: $JEDIT_HOME)" |
|
24 echo |
23 echo |
25 echo " Produce Isabelle/jEdit distribution from Netbeans build" |
24 echo " Produce Isabelle/jEdit distribution from Netbeans build" |
26 echo " in $THIS/dist" |
25 echo " in $THIS/dist" |
27 echo |
26 echo |
28 exit 1 |
27 exit 1 |
64 cd "$THIS/dist" || fail "Bad directory: $THIS/dist" |
63 cd "$THIS/dist" || fail "Bad directory: $THIS/dist" |
65 |
64 |
66 |
65 |
67 # target name |
66 # target name |
68 |
67 |
|
68 [ -z "$JEDIT_HOME" ] && fail "Unknown JEDIT_HOME" |
|
69 |
69 VERSION=$(basename "$JEDIT_HOME") |
70 VERSION=$(basename "$JEDIT_HOME") |
70 JEDIT="jedit-${VERSION}" |
71 JEDIT="jedit-${VERSION}" |
71 |
72 |
72 rm -rf "$JEDIT" jedit |
73 rm -rf "$JEDIT" jedit |
73 mkdir "$JEDIT" |
74 mkdir "$JEDIT" |
74 ln -s "$JEDIT" jedit |
|
75 |
75 |
76 |
76 |
77 # copy stuff |
77 # copy stuff |
78 |
78 |
79 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
79 [ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
93 |
93 |
94 |
94 |
95 # build archive |
95 # build archive |
96 |
96 |
97 echo "${JEDIT}.tar.gz" |
97 echo "${JEDIT}.tar.gz" |
98 tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit |
98 tar czf "${JEDIT}.tar.gz" "$JEDIT" |
99 ln -sf "${JEDIT}.tar.gz" jedit.tar.gz |
|