diff --git a/build/main b/build/main
--- a/build/main
+++ b/build/main
@@ -1,115 +1,115 @@
#!/usr/bin/env bash
#
# Isabelle website build -- main entry point
#
THIS="$(cd "$(dirname "$0")"; pwd)"
SUPER="$(cd "$THIS/.."; pwd)"
## diagnostics
PRG=$(basename "$0")
function usage()
{
echo
echo "Usage: $PRG [-m] DISTBASE OUTPUT"
echo
echo " -m this is a maintainance update, do not update the distribution"
echo
exit 1
}
function fail()
{
echo "$1" >&2
exit 2
}
## arguments and configuration
if [ "$1" = "-m" ] ; then
MAINTAINANCE=true
shift
else
MAINTAINANCE=
fi
[ "$#" -eq 2 ] || usage
DISTBASE="$1"
[ -d "$DISTBASE" ] || fail "Bad distribution: $DISTBASE"
DISTBASE="$(cd "$DISTBASE"; pwd)"
OUTPUT="$2"
mkdir -p "$OUTPUT" || fail "Bad destination: $OUTPUT"
OUTPUT="$(cd "$OUTPUT"; pwd)"
DIST="$(basename "$DISTBASE")"
DISTNAME="${DIST#dist-}"
## copy distribution
if [ ! "$MAINTAINANCE" ] ; then
rsync -v --exclude="/website/" -rltg --chmod g+rw "$DISTBASE" "$OUTPUT/" || fail "Failed"
(
cd "$OUTPUT"
rm -f dist && ln -s "$DIST" dist
rm -f dist/doc && ln -sf "$DISTNAME/doc" dist/doc
cd "$DIST"
if [ ! -d Isabelle/browser_info -a -f "${DISTNAME}_library.tar.gz" ]; then
tar xzf "${DISTNAME}_library.tar.gz"
rm -f library
ln -s "${DISTNAME}/browser_info" library
fi
(
echo ''
echo ''
echo ''
echo ''
echo ''
echo "Isabelle distribution archives"
echo ''
echo 'Isabelle distribution archives
'
for FILE in $(echo *.tar.gz *.exe | tr " " "\n" | sort) $(find contrib -type f | sort)
do
SIZE1="$(du --apparent-size --human-readable "$FILE" | cut -f1)"
SIZE2="$(du --bytes "$FILE" | cut -f1) bytes"
CHECKSUM="$(sha256sum -b "$FILE" | cut -d' ' -f1)"
echo "- SHA256:
${CHECKSUM} $FILE ($SIZE1 / $SIZE2) "
done
echo '
'
) > index.html
)
fi
chgrp -R isabelle "$OUTPUT"
TMPCONTENT="$SUPER"/tmp
mkdir -p "$TMPCONTENT"
"$THIS/mkcontents" -p "//dist/${DISTNAME}/doc/" \
"$DISTBASE/$DISTNAME/doc/Contents" \
"$TMPCONTENT/documentationdist.include.html"
(
echo ''
echo ''
tar xzOf "$DISTBASE/${DISTNAME}.tar.gz" \
"$DISTNAME/lib/html/library_index_content.template" | \
- perl -p -e 's,'
) > "$TMPCONTENT/documentationlib.include.html"
## generate content
env PYTHONPATH="$THIS" "$THIS/buildwebsite" -d "$OUTPUT" distname="$DISTNAME"
EXITVALUE=$?
rm -rf "$TMPCONTENT"
exit "$EXITVALUE"