simplified website/config;
authorwenzelm
Thu, 02 Apr 2009 22:03:04 +0200
changeset 30858 2048e99f4e3e
parent 30857 3fb9345721e4
child 30859 29eb80cef6b7
simplified website/config;
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/