# HG changeset patch
# User wenzelm
# Date 927908458 -7200
# Node ID 0681dd2211b5cd459f5cae8117054cc1702cb10f
# Parent  21f1645f0517e437c678daae7fc6eaa81d6f3c34
move pdfs back into dist;

diff -r 21f1645f0517 -r 0681dd2211b5 Admin/makedist
--- a/Admin/makedist	Fri May 28 18:00:53 1999 +0200
+++ b/Admin/makedist	Fri May 28 18:20:58 1999 +0200
@@ -177,6 +177,9 @@
 $TAR cf $DISTNAME.tar $DISTNAME
 ( cd pdf; $TAR cf ../${DISTNAME}_pdf.tar $DISTNAME; )
 
+mv pdf/$DISTNAME/doc/*.pdf $DISTNAME/doc
+rmdir pdf/$DISTNAME/doc pdf/$DISTNAME
+
 UNPACKED_SIZE=$[ $(cat $DISTNAME.tar ${DISTNAME}_pdf.tar | wc -c) / 1024 ]
 
 gzip $DISTNAME.tar