# HG changeset patch # User wenzelm # Date 1399478948 -7200 # Node ID f901a08c5653c05c4ae18195079343f6df63aff0 # Parent 2f73ef9eb272ad2e0da57531afd6566825c57ae3 explicit option to build library, which takes most of the time; produce minimal index, e.g. for test web page; diff -r 2f73ef9eb272 -r f901a08c5653 Admin/Release/CHECKLIST --- a/Admin/Release/CHECKLIST Wed May 07 14:54:06 2014 +0200 +++ b/Admin/Release/CHECKLIST Wed May 07 18:09:08 2014 +0200 @@ -70,7 +70,7 @@ - fully-automated packaging (requires Mac OS X): - hg up -r DISTNAME && Admin/Release/build -r DISTNAME /home/isabelle/dist + hg up -r DISTNAME && Admin/Release/build -l -r DISTNAME /home/isabelle/dist Final release stage diff -r 2f73ef9eb272 -r f901a08c5653 Admin/Release/build --- a/Admin/Release/build Wed May 07 14:54:06 2014 +0200 +++ b/Admin/Release/build Wed May 07 18:09:08 2014 +0200 @@ -19,6 +19,7 @@ echo echo " Options are:" echo " -j INT maximum number of parallel jobs (default 1)" + echo " -l build library" echo " -r RELEASE proper release with name" echo echo " Make Isabelle distribution DIR, using the local repository clone." @@ -46,15 +47,19 @@ # options JOBS="" +LIBRARY="" RELEASE="" -while getopts "j:r:" OPT +while getopts "j:lr:" OPT do case "$OPT" in j) check_number "$OPTARG" JOBS="-j $OPTARG" ;; + l) + LIBRARY="true" + ;; r) RELEASE="$OPTARG" ;; @@ -89,6 +94,8 @@ ## main +# make dist + if [ -z "$RELEASE" ]; then DISTNAME="Isabelle_$(env LC_ALL=C date "+%d-%b-%Y")" "$ISABELLE_TOOL" makedist -d "$BASE_DIR" $JOBS @@ -101,6 +108,8 @@ DISTBASE="$BASE_DIR/dist-${DISTNAME}" +# make bundles + for PLATFORM_FAMILY in linux macos windows do @@ -112,5 +121,32 @@ done -"$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" + +# minimal index + +cat > "$DISTBASE/index.html" < + + +${DISTNAME} + + +

${DISTNAME}

+ + + +EOF + + +# HTML library + +if [ -n "$LIBRARY" ]; then + "$THIS/build_library" $JOBS "$DISTBASE/${DISTNAME}_${ISABELLE_PLATFORM_FAMILY}.tar.gz" +fi +