equal
deleted
inserted
replaced
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 |