Admin/makedist
changeset 6296 9da8f9262c4c
parent 5817 02f4ff005a78
child 6304 9a82e1c3d9da
equal deleted inserted replaced
6295:351b3c2b0d83 6296:9da8f9262c4c
   154 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML
   154 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML
   155 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   155 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   156 lynx -dump README.html >README
   156 lynx -dump README.html >README
   157 
   157 
   158 
   158 
       
   159 # prepare index.html
       
   160 
       
   161 perl -pi -e \
       
   162  "s/{ISABELLE}/$DISTNAME/g; \
       
   163   s/{PACKED_SIZE}/$PACKED_SIZE/g; \
       
   164   s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
       
   165   s/{AUTHOR}/$LOGNAME/g; \
       
   166   s/{DATE}/$DATE/g;" \
       
   167     ../index.html \
       
   168     lib/html/index1.html \
       
   169     lib/html/index2.html
       
   170 
       
   171 
   159 # create archive
   172 # create archive
   160 
   173 
   161 cd $DISTBASE
   174 cd $DISTBASE
   162 
   175 
   163 chown -R $LOGNAME:isabelle $DISTNAME
   176 chown -R $LOGNAME:isabelle $DISTNAME
   175 gzip $DISTNAME.tar
   188 gzip $DISTNAME.tar
   176 
   189 
   177 PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ]
   190 PACKED_SIZE=$[ $(wc -c <$DISTNAME.tar.gz) / 1024 ]
   178 
   191 
   179 
   192 
   180 # prepare index.html
       
   181 
       
   182 perl -pi -e \
       
   183  "s/{ISABELLE}/$DISTNAME/g; \
       
   184   s/{PACKED_SIZE}/$PACKED_SIZE/g; \
       
   185   s/{UNPACKED_SIZE}/$UNPACKED_SIZE/g; \
       
   186   s/{AUTHOR}/$LOGNAME/g; \
       
   187   s/{DATE}/$DATE/g;" \
       
   188     $DISTBASE/index.html \
       
   189     $DISTBASE/$DISTNAME/lib/html/index1.html \
       
   190     $DISTBASE/$DISTNAME/lib/html/index2.html
       
   191 
       
   192 
       
   193 # final note
   193 # final note
   194 
   194 
   195 echo
   195 echo
   196 echo "That's it. You'll find the distribution in $DISTBASE."
   196 echo "That's it. You'll find the distribution in $DISTBASE."
   197 echo
   197 echo