# HG changeset patch
# User wenzelm
# Date 970161019 -7200
# Node ID 76d029a4c42e429ee354e69c526bf8d394176c17
# Parent  78a0397eaec13fa02cc6ca141fc7e46b3809b2c1
tuned;

diff -r 78a0397eaec1 -r 76d029a4c42e Admin/makedist
--- a/Admin/makedist	Thu Sep 28 19:07:09 2000 +0200
+++ b/Admin/makedist	Thu Sep 28 19:10:19 2000 +0200
@@ -219,7 +219,7 @@
 gzip "$DISTNAME.tar"
 
 echo "${DISTNAME}_pdf.tar.gz"
-( cd pdf; echo "${DISTNAME}_pdf.tar"; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
+( cd pdf; "$TAR" cf "../${DISTNAME}_pdf.tar" "$DISTNAME"; )
 gzip "${DISTNAME}_pdf.tar"
 
 mv "pdf/$DISTNAME/doc/"*.pdf "$DISTNAME/doc"
@@ -243,5 +243,5 @@
 # final note
 
 echo "###"
-echo "### Finished."
+echo "### Finished makedist."
 echo "###"