# HG changeset patch
# User wenzelm
# Date 1165616750 -3600
# Node ID 8b2fd895a7fc8896c5fec9639f90ca2d73ecf715
# Parent  dfac729d306650781273b5d25ce44fb957f440f4
date: forcing LC_ALL=C prevents funny file names;

diff -r dfac729d3066 -r 8b2fd895a7fc Admin/makedist
--- 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"