equal
deleted
inserted
replaced
11 |
11 |
12 export CVSROOT=/usr/proj/isabelle-repository/archive |
12 export CVSROOT=/usr/proj/isabelle-repository/archive |
13 DISTPREFIX=~/tmp/isadist |
13 DISTPREFIX=~/tmp/isadist |
14 |
14 |
15 umask 022 |
15 umask 022 |
16 newgrp isabelle |
|
17 |
16 |
18 |
17 |
19 ## diagnostics |
18 ## diagnostics |
20 |
19 |
21 PRG=$(basename "$0") |
20 PRG=$(basename "$0") |
78 |
77 |
79 DATE=$(date "+%d-%b-%Y") |
78 DATE=$(date "+%d-%b-%Y") |
80 DISTDATE=$(date "+%B %Y") |
79 DISTDATE=$(date "+%B %Y") |
81 |
80 |
82 if [ "$VERSION" = "--" ]; then |
81 if [ "$VERSION" = "--" ]; then |
83 DISTNAME="Isabelle_$DATE_test" |
82 DISTNAME="Isabelle_${DATE}_test" |
84 DISTVERSION="$DISTNAME" |
83 DISTVERSION="$DISTNAME" |
85 EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME" |
84 EXPORT="$THIS/cvs-copy $THIS/.. $DISTNAME" |
86 UNOFFICIAL="" |
85 UNOFFICIAL="" |
87 elif [ "$VERSION" = "-" ]; then |
86 elif [ "$VERSION" = "-" ]; then |
88 DISTNAME="Isabelle_$DATE" |
87 DISTNAME="Isabelle_$DATE" |
216 mv "${DISTNAME}-old/lib/logo/isabelle.gif" . |
215 mv "${DISTNAME}-old/lib/logo/isabelle.gif" . |
217 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" |
216 mv "${DISTNAME}-old/README.html" "${DISTNAME}-old/INSTALL" "$DISTNAME" |
218 mkdir "$DISTNAME/doc" |
217 mkdir "$DISTNAME/doc" |
219 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
218 mv "${DISTNAME}-old/doc/"*.pdf "${DISTNAME}-old/doc/Contents" "$DISTNAME/doc" |
220 |
219 |
|
220 chgrp -R isabelle "$DISTNAME" |
|
221 |
221 rm -rf "${DISTNAME}-old" |
222 rm -rf "${DISTNAME}-old" |
222 |
223 |
223 |
224 |
224 # prepare web pages |
225 # prepare web pages |
225 |
226 |