# HG changeset patch
# User wenzelm
# Date 970076390 -7200
# Node ID 6cbe69107c18f7c92b5d28dde784bdb81c82bd1e
# Parent  16292f1471ad8fda88ef57c579624176e3093b0e
tuned;

diff -r 16292f1471ad -r 6cbe69107c18 Admin/makedist
--- a/Admin/makedist	Wed Sep 27 19:37:32 2000 +0200
+++ b/Admin/makedist	Wed Sep 27 19:39:50 2000 +0200
@@ -214,16 +214,17 @@
 mkdir -p "pdf/$DISTNAME/doc"
 mv "$DISTNAME/doc/"*.pdf "pdf/$DISTNAME/doc"
 
-echo "$DISTNAME.tar"
+echo "$DISTNAME.tar.gz"
 "$TAR" cf "$DISTNAME.tar" Isabelle "$DISTNAME"
+gzip "$DISTNAME.tar"
+
+echo "${DISTNAME}_pdf.tar.gz"
 ( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
+gzip "${DISTNAME}_pdf.tar"
 
 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
 rmdir "pdf/$DISTNAME/doc" "pdf/$DISTNAME" pdf
 
-echo "$DISTNAME.tar.gz" && gzip "$DISTNAME.tar"
-echo "${DISTNAME}_pdf.tar.gz" && gzip "${DISTNAME}_pdf.tar"
-
 
 # cleanup dist
 
diff -r 16292f1471ad -r 6cbe69107c18 Admin/page/Makefile
--- a/Admin/page/Makefile	Wed Sep 27 19:37:32 2000 +0200
+++ b/Admin/page/Makefile	Wed Sep 27 19:39:50 2000 +0200
@@ -38,9 +38,6 @@
 # --- begin rules
 
 all: clean main dist install weblint
-	@echo "###"
-	@echo "### Finished.  See main/ and dist/ for the resulting pages."
-	@echo "###"
 
 main:
 	@$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)