Admin/makedist_mercurial

   cat <<EOF
 
 Usage: $PRG [OPTIONS] [VERSION]
 
   Options are:
-    -r NAME         proper release with name"
-
-  Make Isabelle distribution from the Mercurial repository at TUM.
+    -r RELEASE         proper release with name"
+
+  Make Isabelle distribution from the main Mercurial repository at TUM.
 
   VERSION identifies the snapshot, using usual Mercurial terminology;
-  the default is "tip", or the proper release name if given.
+  the default is RELEASE if given, otherwise "tip".
 
 EOF
   exit 1
 }
 

 
 # args
 
 VERSION=""
 [ "$#" -gt 0 ] && { VERSION="$1"; shift; }
+[ -z "$VERSION" ] && VERSION="$RELEASE"
+[ -z "$VERSION" ] && VERSION="tip"
 
 [ "$#" -gt 0 ] && usage
-
-
-# defaults
-
-if [ -z "$RELEASE" ]; then
-  [ -z "$VERSION" ] && VERSION=tip
-else
-  [ -z "$VERSION" ] && VERSION="$RELEASE"
-fi
 
 
 ## main
 
 # tmp

 
 mkdir "$DISTPREFIX/$TMP" || fail "Failed to create fresh directory"
 cd "$DISTPREFIX/$TMP"
 
 echo "###"
-echo "### Retrieving Mercurial snapshot ${VERSION}.tar.gz"
-echo "###"
-
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" && tar -x -z -f "${VERSION}.tar.gz"; } || \
+echo "### Retrieving Mercurial snapshot $VERSION"
+echo "###"
+
+{ wget -q "$REPOS/archive/${VERSION}.tar.gz" -O- | tar -xzf -; } || \
   fail "Failed to retrieve $VERSION"
 
-rm "${VERSION}.tar.gz"
 IDENT=$(echo * | sed 's/Isabelle-repository-//')
 
 rm -f "Isabelle-repository-$IDENT/.hg_archival.txt"
 rm -f "Isabelle-repository-$IDENT/.hgtags"
 

 # website
 
 mkdir -p ../website
 cat > ../website/distinfo.mak <<EOF
 # this is a generated file - do not edit unless you know what you are doing!
-
 DISTNAME=$DISTNAME
 DISTBASE=$DISTBASE
 EOF
 
 cp lib/html/library_index_content.template ../website/

 
 mkdir -p "pdf/$DISTNAME/doc"
 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
 
 echo "$DISTNAME.tar.gz"
-tar -c -z -f "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
+tar -czf "$DISTNAME.tar.gz" Isabelle "$DISTNAME"
 
 echo "${DISTNAME}_pdf.tar.gz"
-tar -C pdf -c -z -f "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
+tar -C pdf -czf "${DISTNAME}_pdf.tar.gz" "$DISTNAME"
 
 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
 
 

 
 chgrp -R isabelle "$DISTNAME"
 
 rm -rf "${DISTNAME}-old"
 
-echo "###"
-echo "### Finished makedist."
-echo "###"