equal
deleted
inserted
replaced
170 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
170 perl -pi -e "s,{ISABELLE},$DISTNAME,g" lib/html/library_index_header.template |
171 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
171 perl -pi -e "s,unidentified repository version,$DISTVERSION,g" src/Pure/ROOT.ML lib/Tools/version |
172 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README |
172 perl -pi -e "s,some unidentified repository version of Isabelle,$DISTVERSION,g" README |
173 |
173 |
174 |
174 |
175 # create archives |
175 # create archive |
176 |
176 |
177 echo "###" |
177 echo "###" |
178 echo "### Creating archives ..." |
178 echo "### Creating archive ..." |
179 echo "###" |
179 echo "###" |
180 |
180 |
181 cd "$DISTBASE" |
181 cd "$DISTBASE" |
182 |
182 |
183 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
183 echo "$DISTBASE/$DISTNAME.tar.gz" > ../ISABELLE_DIST |
208 |
208 |
209 chgrp -R isabelle "$DISTNAME" |
209 chgrp -R isabelle "$DISTNAME" |
210 |
210 |
211 rm -rf "${DISTNAME}-old" |
211 rm -rf "${DISTNAME}-old" |
212 |
212 |
|
213 |
|
214 echo "DONE" |