equal
deleted
inserted
replaced
188 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
188 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
189 echo |
189 echo |
190 } >ANNOUNCE |
190 } >ANNOUNCE |
191 fi |
191 fi |
192 |
192 |
193 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html |
193 perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/library_index_header.html |
194 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version |
194 perl -pi -e "s/Isabelle repository version/$DISTVERSION/" src/Pure/ROOT.ML lib/Tools/version |
195 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README |
195 perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README |
196 |
196 |
197 ( cd src; ../Admin/maketags; ) |
197 ( cd src; ../Admin/maketags; ) |
198 |
198 |