# HG changeset patch # User wenzelm # Date 1238965959 -7200 # Node ID 0a667739d175f9bbb8c24d36c3a31b7330660126 # Parent 71fde5b7b43c421bd38cd081152865750f693653# Parent 104b13484feb9a8abe5a9f500432019bbac04d30 merged diff -r 71fde5b7b43c -r 0a667739d175 Admin/makedist --- a/Admin/makedist Sun Apr 05 19:21:51 2009 +0100 +++ b/Admin/makedist Sun Apr 05 23:12:39 2009 +0200 @@ -125,17 +125,6 @@ cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME" -# website - -mkdir -p ../website -cat > ../website/config <