Admin/makedist
changeset 6304 9a82e1c3d9da
parent 6296 9da8f9262c4c
child 6630 5f810292c030
--- a/Admin/makedist	Wed Mar 03 11:27:10 1999 +0100
+++ b/Admin/makedist	Thu Mar 04 14:23:51 1999 +0100
@@ -151,24 +151,12 @@
   } >UNOFFICIAL
 fi
 
+perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index1.html lib/html/index2.html
 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML
 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
 lynx -dump README.html >README
 
 
-# prepare index.html
-
-perl -pi -e \
- "s/{ISABELLE}/$DISTNAME/g; \
-  s/{PACKED_SIZE}/$PACKED_SIZE/g; \
-  s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
-  s/{AUTHOR}/$LOGNAME/g; \
-  s/{DATE}/$DATE/g;" \
-    ../index.html \
-    lib/html/index1.html \
-    lib/html/index2.html
-
-
 # create archive
 
 cd $DISTBASE
@@ -190,6 +178,17 @@
 PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ]
 
 
+# prepare dist index.html
+
+perl -pi -e \
+ "s/{ISABELLE}/$DISTNAME/g; \
+  s/{PACKED_SIZE}/$PACKED_SIZE/g; \
+  s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
+  s/{AUTHOR}/$LOGNAME/g; \
+  s/{DATE}/$DATE/g;" \
+    index.html
+
+
 # final note
 
 echo