Admin/makedist
changeset 3257 4e3724e0659f
parent 3186 57be77ca36ff
child 3281 d4ddd43f418a
equal deleted inserted replaced
3256:0a45cdd7da37 3257:4e3724e0659f
   141     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   141     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   142     echo
   142     echo
   143   } >UNOFFICIAL
   143   } >UNOFFICIAL
   144 fi
   144 fi
   145 
   145 
       
   146 lynx -dump README.html >README
       
   147 
   146 
   148 
   147 # create archive
   149 # create archive
   148 
   150 
   149 cd $DISTBASE
   151 cd $DISTBASE
   150 
   152