changeset 21712 | 8b2fd895a7fc |
parent 20990 | 0c1296049b47 |
child 23149 | ddc5800b699f |
1.1 --- a/Admin/makedist Fri Dec 08 22:17:20 2006 +0100 1.2 +++ b/Admin/makedist Fri Dec 08 23:25:50 2006 +0100 1.3 @@ -80,8 +80,8 @@ 1.4 1.5 # dist version 1.6 1.7 -DATE=$(date "+%d-%b-%Y") 1.8 -DISTDATE=$(date "+%B %Y") 1.9 +DATE=$(env LC_ALL=C date "+%d-%b-%Y") 1.10 +DISTDATE=$(env LC_ALL=C date "+%B %Y") 1.11 1.12 if [ "$VERSION" = "-" ]; then 1.13 DISTIDENT="Isabelle_$DATE"