diff -r 180e28bab764 -r 0f8e2dcabbf9 Admin/makedist_mercurial
--- a/Admin/makedist_mercurial	Fri Jul 18 18:25:57 2008 +0200
+++ b/Admin/makedist_mercurial	Fri Jul 18 22:03:20 2008 +0200
@@ -25,12 +25,12 @@
 Usage: $PRG [OPTIONS] [VERSION]
 
   Options are:
-    -r NAME         proper release with name"
+    -r RELEASE         proper release with name"
 
-  Make Isabelle distribution from the Mercurial repository at TUM.
+  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
@@ -68,19 +68,12 @@
 
 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
@@ -95,13 +88,12 @@
 cd "$DISTPREFIX/$TMP"
 
 echo "###"
-echo "### Retrieving Mercurial snapshot ${VERSION}.tar.gz"
+echo "### Retrieving Mercurial snapshot $VERSION"
 echo "###"
 
-{ wget -q "$REPOS/archive/${VERSION}.tar.gz" && tar -x -z -f "${VERSION}.tar.gz"; } || \
+{ 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"
@@ -138,7 +130,6 @@
 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
@@ -214,10 +205,10 @@
 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
@@ -238,6 +229,3 @@
 
 rm -rf "${DISTNAME}-old"
 
-echo "###"
-echo "### Finished makedist."
-echo "###"