Admin/makedist
changeset 4986 d4f257d3445a
parent 4982 6f96354267e0
child 5169 c677baeac0f7
equal deleted inserted replaced
4985:aaaf64da9e3a 4986:d4f257d3445a
   147     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   147     echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE."
   148     echo
   148     echo
   149   } >UNOFFICIAL
   149   } >UNOFFICIAL
   150 fi
   150 fi
   151 
   151 
   152 perl -pi -e "s/Internal working version of Isabelle/$DISTVERSION/" src/Pure/ROOT.ML
   152 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML
   153 perl -pi -e "s/an internal working version of Isabelle/$DISTVERSION/" README.html
   153 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
   154 lynx -dump README.html >README
   154 lynx -dump README.html >README
   155 
   155 
   156 
   156 
   157 # create archive
   157 # create archive
   158 
   158