author | wenzelm |
Fri, 08 Dec 2006 23:25:50 +0100 | |
changeset 21712 | 8b2fd895a7fc |
parent 21711 | dfac729d3066 |
child 21713 | 85722dc0fc81 |
Admin/makedist | file | annotate | diff | comparison | revisions |
--- a/Admin/makedist Fri Dec 08 22:17:20 2006 +0100 +++ b/Admin/makedist Fri Dec 08 23:25:50 2006 +0100 @@ -80,8 +80,8 @@ # dist version -DATE=$(date "+%d-%b-%Y") -DISTDATE=$(date "+%B %Y") +DATE=$(env LC_ALL=C date "+%d-%b-%Y") +DISTDATE=$(env LC_ALL=C date "+%B %Y") if [ "$VERSION" = "-" ]; then DISTIDENT="Isabelle_$DATE"