Admin/makedist
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"