# HG changeset patch
# User wenzelm
# Date 1238702584 -7200
# Node ID 2048e99f4e3eec7210d9ac5d59b7f61386d77ab3
# Parent  3fb9345721e4ac49536173cdacb7a92f0e79a148
simplified website/config;

diff -r 3fb9345721e4 -r 2048e99f4e3e Admin/makedist
--- a/Admin/makedist	Thu Apr 02 16:18:19 2009 +0200
+++ b/Admin/makedist	Thu Apr 02 22:03:04 2009 +0200
@@ -128,10 +128,9 @@
 # website
 
 mkdir -p ../website
-cat > ../website/distinfo.mak <<EOF
-# this is a generated file - do not edit unless you know what you are doing!
-DISTNAME=$DISTNAME
-DISTBASE=$DISTBASE
+cat > ../website/config <<EOF
+DISTNAME="$DISTNAME"
+DISTBASE="$DISTBASE"
 EOF
 
 cp lib/html/library_index_content.template ../website/