165 cd $DISTBASE |
166 cd $DISTBASE |
166 |
167 |
167 chown -R $LOGNAME:isabelle $DISTNAME |
168 chown -R $LOGNAME:isabelle $DISTNAME |
168 chmod -R u+w $DISTNAME |
169 chmod -R u+w $DISTNAME |
169 |
170 |
170 if type -path gtar |
171 TAR=tar |
171 then |
172 type -path gtar >/dev/null && TAR=gtar |
172 gtar cf $DISTNAME.tar $DISTNAME |
173 |
173 else |
174 mkdir -p pdf/$DISTNAME/doc |
174 tar cf $DISTNAME.tar $DISTNAME |
175 mv $DISTNAME/doc/*.pdf pdf/$DISTNAME/doc |
175 fi |
176 |
176 |
177 $TAR cf $DISTNAME.tar $DISTNAME |
177 UNPACKED_SIZE=$[ $(wc -c <$DISTNAME.tar) / 1024 ] |
178 ( cd pdf; $TAR cf ../${DISTNAME}_pdf.tar $DISTNAME; ) |
|
179 |
|
180 UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ] |
178 |
181 |
179 gzip $DISTNAME.tar |
182 gzip $DISTNAME.tar |
|
183 gzip ${DISTNAME}_pdf.tar |
180 |
184 |
181 PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ] |
185 PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ] |
|
186 PACKED_SIZE_PDF=$[ $(wc -c <${DISTNAME}_pdf.tar.gz) / 1024 ] |
182 |
187 |
183 |
188 |
184 # prepare dist index.html |
189 # prepare dist index.html |
185 |
190 |
186 perl -pi -e \ |
191 perl -pi -e \ |
187 "s/{ISABELLE}/$DISTNAME/g; \ |
192 "s/{ISABELLE}/$DISTNAME/g; \ |
188 s/{PACKED_SIZE}/$PACKED_SIZE/g; \ |
193 s/{PACKED_SIZE}/$PACKED_SIZE/g; \ |
|
194 s/{PACKED_SIZE_PDF}/$PACKED_SIZE_PDF/g; \ |
189 s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ |
195 s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \ |
190 s/{AUTHOR}/$LOGNAME/g; \ |
196 s/{AUTHOR}/$LOGNAME/g; \ |
191 s/{DATE}/$DATE/g;" \ |
197 s/{DATE}/$DATE/g;" \ |
192 index.html |
198 index.html |
193 |
199 |