author | immler@in.tum.de |
Sun, 01 Feb 2009 13:57:59 +0100 | |
changeset 34516 | 73225f520f8c |
parent 34512 | 14d70378f1c7 |
child 34519 | 92f50a3b4a6a |
permissions | -rwxr-xr-x |
34332 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# makedist -- make Isabelle/jEdit distribution |
|
4 |
||
5 |
## self references |
|
6 |
||
7 |
PRG=$(basename "$0") |
|
8 |
THIS=$(cd "$(dirname "$0")"; pwd) |
|
9 |
SUPER=$(cd "$THIS/.."; pwd) |
|
10 |
||
11 |
||
12 |
## diagnostics |
|
13 |
||
34414 | 14 |
JEDIT_HOME="/home/isajedit/jedit-orig/4.3pre16" |
34332 | 15 |
|
16 |
function usage() |
|
17 |
{ |
|
18 |
echo |
|
19 |
echo "Usage: $PRG [OPTIONS]" |
|
20 |
echo |
|
21 |
echo " Options are:" |
|
22 |
echo " -j DIR specify original jEdit distribution" |
|
23 |
echo " (default: $JEDIT_HOME)" |
|
24 |
echo |
|
25 |
echo " Produce Isabelle/jEdit distribution from Netbeans build" |
|
26 |
echo " in $THIS/dist" |
|
27 |
echo |
|
28 |
exit 1 |
|
29 |
} |
|
30 |
||
31 |
fail() |
|
32 |
{ |
|
33 |
echo "$1" >&2 |
|
34 |
exit 2 |
|
35 |
} |
|
36 |
||
37 |
||
38 |
## process command line |
|
39 |
||
40 |
# options |
|
41 |
||
42 |
while getopts "j:s:" OPT |
|
43 |
do |
|
44 |
case "$OPT" in |
|
45 |
j) |
|
46 |
JEDIT_HOME="$OPTARG" |
|
47 |
;; |
|
48 |
\?) |
|
49 |
usage |
|
50 |
;; |
|
51 |
esac |
|
52 |
done |
|
53 |
||
54 |
shift $(($OPTIND - 1)) |
|
55 |
||
56 |
||
57 |
# args |
|
58 |
||
59 |
[ "$#" -ne 0 ] && usage |
|
60 |
||
61 |
||
62 |
## main |
|
63 |
||
64 |
cd "$THIS/dist" || fail "Bad directory: $THIS/dist" |
|
65 |
||
66 |
||
67 |
# target name |
|
68 |
||
69 |
VERSION=$(basename "$JEDIT_HOME") |
|
70 |
JEDIT="jedit-${VERSION}" |
|
71 |
||
72 |
rm -rf "$JEDIT" jedit |
|
73 |
mkdir "$JEDIT" |
|
74 |
ln -s "$JEDIT" jedit |
|
75 |
||
76 |
||
77 |
# copy stuff |
|
78 |
||
79 |
[ "$JEDIT_HOME/jedit.jar" ] || fail "Bad original jEdit directory: $JEDIT_HOME" |
|
80 |
cp -R "$JEDIT_HOME/." "$JEDIT/." |
|
34478
095e5cae6656
removed jEdit/build-support (belongs to src distribution);
wenzelm
parents:
34469
diff
changeset
|
81 |
rm -rf "$JEDIT/jEdit" "$JEDIT/build-support" |
34332 | 82 |
|
34512
14d70378f1c7
modified netbeans build such that dist can be used as settings-directory for jedit;
immler@in.tum.de
parents:
34478
diff
changeset
|
83 |
cp -R jars "$JEDIT/jars" |
34332 | 84 |
|
85 |
cp -R "$THIS/dist-template/." "$JEDIT/." |
|
86 |
||
34419 | 87 |
perl -i -e 'while (<>) { if (m/NAME="javacc"/) { |
88 |
print qq,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,; } |
|
89 |
print; }' "$JEDIT/modes/catalog" |
|
90 |
||
34332 | 91 |
# build archive |
92 |
||
93 |
echo "${JEDIT}.tar.gz" |
|
94 |
tar czf "${JEDIT}.tar.gz" "$JEDIT" jedit |
|
95 |
ln -sf "${JEDIT}.tar.gz" jedit.tar.gz |