Admin/makedist
changeset 30858 2048e99f4e3e
parent 30287 39b931e00ba9
child 30870 61f2131554cd
equal deleted inserted replaced
30857:3fb9345721e4 30858:2048e99f4e3e
   126 
   126 
   127 
   127 
   128 # website
   128 # website
   129 
   129 
   130 mkdir -p ../website
   130 mkdir -p ../website
   131 cat > ../website/distinfo.mak <<EOF
   131 cat > ../website/config <<EOF
   132 # this is a generated file - do not edit unless you know what you are doing!
   132 DISTNAME="$DISTNAME"
   133 DISTNAME=$DISTNAME
   133 DISTBASE="$DISTBASE"
   134 DISTBASE=$DISTBASE
       
   135 EOF
   134 EOF
   136 
   135 
   137 cp lib/html/library_index_content.template ../website/
   136 cp lib/html/library_index_content.template ../website/
   138 
   137 
   139 
   138