equal
deleted
inserted
replaced
163 fi |
163 fi |
164 |
164 |
165 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML |
165 perl -pi -e "s,val changelog = \"\",val changelog = \"$REPOS/log/$IDENT\",g" src/Pure/ROOT.ML |
166 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings |
166 perl -pi -e "s,ISABELLE_IDENTIFIER=\"\",ISABELLE_IDENTIFIER=\"$DISTNAME\",g" lib/scripts/getsettings |
167 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
167 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
168 perl -pi -e "s,Isabelle repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
168 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
169 perl -pi -e "s,the internal repository version of Isabelle,$DISTVERSION,g" README |
169 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README |
170 |
170 |
171 |
171 |
172 # create archives |
172 # create archives |
173 |
173 |
174 echo "###" |
174 echo "###" |