equal
deleted
inserted
replaced
74 ## main |
74 ## main |
75 |
75 |
76 # dist version |
76 # dist version |
77 |
77 |
78 DATE=$(date "+%d-%b-%Y") |
78 DATE=$(date "+%d-%b-%Y") |
|
79 DISTDATE=$(date "+%B %Y") |
79 |
80 |
80 if [ "$VERSION" = "-" ]; then |
81 if [ "$VERSION" = "-" ]; then |
81 DISTNAME=Isabelle_$DATE |
82 DISTNAME=Isabelle_$DATE |
82 EXPORT="checkout -P" |
83 EXPORT="checkout -P" |
83 UNOFFICIAL=true |
84 UNOFFICIAL=true |
144 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
145 echo "This is an unofficial release of Isabelle, created by $LOGNAME $DATE." |
145 echo |
146 echo |
146 } >UNOFFICIAL |
147 } >UNOFFICIAL |
147 fi |
148 fi |
148 |
149 |
|
150 perl -pi -e "s/Internal working version of Isabelle/$DISTNAME: $DISTDATE/" src/Pure/ROOT.ML |
|
151 perl -pi -e "s/an internal working version of Isabelle/$DISTNAME: $DISTDATE/" README.html |
149 lynx -dump README.html >README |
152 lynx -dump README.html >README |
150 |
153 |
151 |
154 |
152 # create archive |
155 # create archive |
153 |
156 |