# HG changeset patch
# User wenzelm
# Date 1238963102 -7200
# Node ID 61f2131554cd01097cb65480c3fabd47ed388656
# Parent  5106e13d400fa6af8afdc17cca9c645fd1f9edbc
removed obsolete website directory -- information derived by website/build;

diff -r 5106e13d400f -r 61f2131554cd Admin/makedist
--- a/Admin/makedist	Fri Apr 03 18:03:29 2009 +0200
+++ b/Admin/makedist	Sun Apr 05 22:25:02 2009 +0200
@@ -125,17 +125,6 @@
 cd "$DISTNAME" || fail "No dist directory: $DISTBASE/$DISTNAME"
 
 
-# website
-
-mkdir -p ../website
-cat > ../website/config <<EOF
-DISTNAME="$DISTNAME"
-DISTBASE="$DISTBASE"
-EOF
-
-cp lib/html/library_index_content.template ../website/
-
-
 # prepare dist for release
 
 echo "###"