author  hoelzl 
Wed, 09 Apr 2014 09:37:48 +0200  
changeset 56480  093ea91498e6 
parent 53913  5ff12177a067 
child 57649  a43898f76ae9 
permissions  rwxrxrx 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

1 
#!/usr/bin/env bash 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

2 
# 
49004  3 
# Author: Makarius 
4 
# 

5 
# DESCRIPTION: make Isabelle distribution from repository 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

6 

49004  7 
## global parameters 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

8 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

9 
umask 022 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

10 

49004  11 
HG="${HG:hg}" 
12 

13 
DISTPREFIX="${DISTPREFIX:$HOME/tmp/isadist}" 

14 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

15 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

16 
## diagnostics 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

17 

30885  18 
PRG="$(basename "$0")" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

19 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

20 
function usage() 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

21 
{ 
49004  22 
echo 
23 
echo "Usage: isabelle $PRG [OPTIONS] [VERSION]" 

24 
echo 

25 
echo " Options are:" 

26 
echo " d DIR global directory prefix (default: \"$DISTPREFIX\")" 

27 
echo " j INT maximum number of parallel jobs (default 1)" 

28 
echo " r RELEASE proper release with name" 

29 
echo 

30 
echo " Make Isabelle distribution from the local repository clone." 

31 
echo 

32 
echo " VERSION identifies the snapshot, using usual Mercurial terminology;" 

33 
echo " the default is RELEASE if given, otherwise \"tip\"." 

34 
echo 

50789  35 
echo " Addon components are that of the running Isabelle version!" 
49004  36 
echo 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

37 
exit 1 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

38 
} 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

39 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

40 
function fail() 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

41 
{ 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

42 
echo "$1" >&2 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

43 
exit 2 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

44 
} 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

45 

49004  46 
function check_number() 
47 
{ 

48 
[ n "$1" a z "$(echo "$1"  tr d '[09]')" ]  fail "Bad number: \"$1\"" 

49 
} 

50 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

51 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

52 
## process command line 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

53 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

54 
# options 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

55 

49004  56 
JOBS="" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

57 
RELEASE="" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

58 

49004  59 
while getopts "d:j:r:" OPT 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

60 
do 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

61 
case "$OPT" in 
49004  62 
d) 
63 
DISTPREFIX="$OPTARG" 

64 
;; 

43357
07889e32bc58
makedist j: build Isabelle/jEdit via given jedit_build component;
wenzelm
parents:
41984
diff
changeset

65 
j) 
49004  66 
check_number "$OPTARG" 
67 
JOBS="j $OPTARG" 

43357
07889e32bc58
makedist j: build Isabelle/jEdit via given jedit_build component;
wenzelm
parents:
41984
diff
changeset

68 
;; 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

69 
r) 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

70 
RELEASE="$OPTARG" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

71 
;; 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

72 
\?) 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

73 
usage 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

74 
;; 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

75 
esac 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

76 
done 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

77 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

78 
shift $(($OPTIND  1)) 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

79 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

80 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

81 
# args 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

82 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

83 
VERSION="" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

84 
[ "$#" gt 0 ] && { VERSION="$1"; shift; } 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

85 
[ z "$VERSION" ] && VERSION="$RELEASE" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

86 
[ z "$VERSION" ] && VERSION="tip" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

87 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

88 
[ "$#" gt 0 ] && usage 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

89 

49004  90 
IDENT=$("$HG" repository "$ISABELLE_HOME" id r "$VERSION" i) 
91 
[ z "$IDENT" ] && fail "Bad repository version: \"$VERSION\"" 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

92 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

93 

49004  94 
## main 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

95 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

96 
# dist name 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

97 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

98 
DATE=$(env LC_ALL=C date "+%d%b%Y") 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

99 
DISTDATE=$(env LC_ALL=C date "+%B %Y") 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

100 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

101 
if [ z "$RELEASE" ]; then 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

102 
DISTNAME="Isabelle_$DATE" 
40573  103 
DISTVERSION="Isabelle repository snapshot $IDENT $DATE" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

104 
else 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

105 
DISTNAME="$RELEASE" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

106 
DISTVERSION="$DISTNAME: $DISTDATE" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

107 
fi 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

108 

51073  109 
DISTPREFIX="$(cd "$DISTPREFIX"; pwd)" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

110 
DISTBASE="$DISTPREFIX/dist$DISTNAME" 
49004  111 
mkdir p "$DISTBASE"  fail "Unable to create distribution base dir \"$DISTBASE\"" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

112 

49004  113 
DIR="$DISTBASE/$DISTNAME" 
114 
[ e "$DIR" ] && fail "Directory \"$DIR\" already exists" 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

115 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

116 

49004  117 
# retrieve repository archive 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

118 

49004  119 
echo "### Retrieving Mercurial repository $VERSION" 
47010  120 

49004  121 
"$HG" repository "$ISABELLE_HOME" archive type files r "$IDENT" "$DIR"  \ 
122 
fail "Failed to retrieve $VERSION" 

43357
07889e32bc58
makedist j: build Isabelle/jEdit via given jedit_build component;
wenzelm
parents:
41984
diff
changeset

123 

49004  124 
rm f "$DIR/.hg_archival.txt" 
125 
rm f "$DIR/.hgtags" 

126 
rm f "$DIR/.hgignore" 

127 
rm f "$DIR/README_REPOSITORY" 

128 

43357
07889e32bc58
makedist j: build Isabelle/jEdit via given jedit_build component;
wenzelm
parents:
41984
diff
changeset

129 

49004  130 
# partial context switch to new version 
48606
4b6c90e121b1
makedist D retains docsrc component with its "doc" sessions (relevant for testing);
wenzelm
parents:
48190
diff
changeset

131 

49004  132 
cd "$DIR" 
133 

134 
unset ISABELLE_SETTINGS_PRESENT 

135 
unset ISABELLE_SITE_SETTINGS_PRESENT 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

136 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

137 
if [ z "$RELEASE" ]; then 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

138 
{ 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

139 
echo 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

140 
echo "IMPORTANT NOTE" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

141 
echo "==============" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

142 
echo 
53436  143 
echo "This is a snapshot of Isabelle/${IDENT} from the repository." 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

144 
echo 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

145 
} >ANNOUNCE 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

146 
else 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

147 
perl pi e "s,val is_official = false,val is_official = true,g" src/Pure/ROOT.ML 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

148 
fi 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

149 

41511  150 
perl pi e "s,ISABELLE_ID=\"\",ISABELLE_ID=\"$IDENT\",g" lib/scripts/getsettings 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

151 
perl pi e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

152 
perl pi e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template 
32361
141e5151b918
clarified situation about unidentified repository versions  in a distributed setting there is not "the" repository;
wenzelm
parents:
31842
diff
changeset

153 
perl pi e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version 
141e5151b918
clarified situation about unidentified repository versions  in a distributed setting there is not "the" repository;
wenzelm
parents:
31842
diff
changeset

154 
perl pi e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

155 

49004  156 
mkdir p contrib 
157 
cat >contrib/README <<EOF 

158 
This directory contains addon components that contribute to the main 

159 
Isabelle distribution. Separate licensing conditions apply, see each 

160 
directory individually. 

161 
EOF 

162 

163 

164 
# prepare dist for release 

165 

166 
echo "### Preparing distribution $DISTNAME" 

167 

168 
find . "(" name \*.thy o name \*.ML o name \*.scala ")" perm +111 print  xargs chmod f x 

169 
find . print  xargs chmod f u+rw 

170 

53579  171 
export CLASSPATH="$ISABELLE_CLASSPATH" 
172 

49004  173 
./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS optimise" \ 
174 
./Admin/build all  fail "Failed to build distribution" 

175 

50797  176 
./bin/isabelle env ISABELLE_SCALA_BUILD_OPTIONS="$ISABELLE_SCALA_BUILD_OPTIONS optimise" \ 
177 
./bin/isabelle jedit b  fail "Failed to build Isabelle/jEdit" 

49004  178 

50797  179 
cp a src src.orig 
180 
env ISABELLE_IDENTIFIER="${DISTNAME}build" \ 

53208
bec95e287d26
prefer build_doc s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents:
51073
diff
changeset

181 
./bin/isabelle build_doc $JOBS s a  fail "Failed to build documentation" 
50797  182 
rm rf src 
183 
mv src.orig src 

49004  184 

53208
bec95e287d26
prefer build_doc s to avoid heaps left behind in $ISABELLE_HOME_USER (especially relevant to isatest);
wenzelm
parents:
51073
diff
changeset

185 
rm rf Admin browser_info heaps 
49004  186 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

187 

37341  188 
# create archive 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

189 

49004  190 
echo "### Creating archive" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

191 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

192 
cd "$DISTBASE" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

193 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

194 
echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

195 
echo "$IDENT" >../ISABELLE_IDENT 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

196 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

197 
chown R "$LOGNAME" "$DISTNAME" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

198 
chmod R u+w "$DISTNAME" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

199 
chmod R g=o "$DISTNAME" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

200 

49007  201 
echo "$DISTBASE/$DISTNAME.tar.gz" 
53913
5ff12177a067
prefer GNU tar for Isabelle to avoid odd extended header keywords produced by Apple's bsdtar (see also 8f6046b7f850);
wenzelm
parents:
53579
diff
changeset

202 
tar c z f "$DISTNAME.tar.gz" "$DISTNAME" 
50899
506ff6abfde0
grandunified Admin/Release/build script (excluding .app and .exe);
wenzelm
parents:
50863
diff
changeset

203 
[ "$?" = 0 ]  exit "$?" 
28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

204 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

205 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

206 
# cleanup dist 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

207 

ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

208 
mv "$DISTNAME" "${DISTNAME}old" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

209 
mkdir "$DISTNAME" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

210 

37368  211 
mv "${DISTNAME}old/README" "${DISTNAME}old/NEWS" "${DISTNAME}old/ANNOUNCE" \ 
212 
"${DISTNAME}old/COPYRIGHT" "${DISTNAME}old/CONTRIBUTORS" "$DISTNAME" 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

213 
mkdir "$DISTNAME/doc" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

214 
mv "${DISTNAME}old/doc/"*.pdf "${DISTNAME}old/doc/Contents" "$DISTNAME/doc" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

215 

41984
e5dba3d75e9e
recover Isabelle symlink for public distribution, notably website;
wenzelm
parents:
41665
diff
changeset

216 
rm f Isabelle && ln sf "$DISTNAME" Isabelle 
e5dba3d75e9e
recover Isabelle symlink for public distribution, notably website;
wenzelm
parents:
41665
diff
changeset

217 

28932
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

218 
rm rf "${DISTNAME}old" 
ccaa3355f7d3
makedist  make Isabelle source distribution (Mercurial version);
wenzelm
parents:
diff
changeset

219 