equal
deleted
inserted
replaced
155 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
155 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
156 echo |
156 echo |
157 } >UNOFFICIAL |
157 } >UNOFFICIAL |
158 fi |
158 fi |
159 |
159 |
160 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index1.html lib/html/index2.html |
160 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html |
161 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML |
161 perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML |
162 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html |
162 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html |
163 lynx -dump README.html >README |
163 lynx -dump README.html >README |
164 |
164 |
165 |
165 |