Admin/makedist
changeset 30858 2048e99f4e3e
parent 30287 39b931e00ba9
child 30870 61f2131554cd
     1.1 --- a/Admin/makedist	Thu Apr 02 16:18:19 2009 +0200
     1.2 +++ b/Admin/makedist	Thu Apr 02 22:03:04 2009 +0200
     1.3 @@ -128,10 +128,9 @@
     1.4  # website
     1.5  
     1.6  mkdir -p ../website
     1.7 -cat > ../website/distinfo.mak <<EOF
     1.8 -# this is a generated file - do not edit unless you know what you are doing!
     1.9 -DISTNAME=$DISTNAME
    1.10 -DISTBASE=$DISTBASE
    1.11 +cat > ../website/config <<EOF
    1.12 +DISTNAME="$DISTNAME"
    1.13 +DISTBASE="$DISTBASE"
    1.14  EOF
    1.15  
    1.16  cp lib/html/library_index_content.template ../website/