tuned;
authorwenzelm
Thu, 22 Oct 1998 11:09:43 +0200
changeset 5725 26772f4543fc
parent 5724 a9f8cb9b5b5d
child 5726 5de7e399ec88
tuned;
Admin/makedist
--- a/Admin/makedist	Thu Oct 22 10:58:50 1998 +0200
+++ b/Admin/makedist	Thu Oct 22 11:09:43 1998 +0200
@@ -184,7 +184,8 @@
   s/{PACKED_SIZE}/$PACKED_SIZE/g; \
   s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
   s/{AUTHOR}/$LOGNAME/g; \
-  s/{DATE}/$DATE/g;" index.html $DISTNAME/lib/html/index1.html $DISTNAME/lib/html/index2.html
+  s/{DATE}/$DATE/g;" \
+    $DISTBASE/index.html $DISTNAME/lib/html/index1.html $DISTNAME/lib/html/index2.html
 
 
 # final note