# HG changeset patch
# User haftmann
# Date 1118059927 -7200
# Node ID f9f2e16435936157b39f7d87652d349991d8520b
# Parent  a4e163c7ed9c18bb86156333dc71b4dc9846bdfa
migrated scripts to new webiste

diff -r a4e163c7ed9c -r f9f2e1643593 Admin/make_everything
--- a/Admin/make_everything	Mon Jun 06 14:11:05 2005 +0200
+++ b/Admin/make_everything	Mon Jun 06 14:12:07 2005 +0200
@@ -33,7 +33,6 @@
 cd $(dirname "$ISABELLE_DIST")
 cp -a ../contrib .
 
-cd page && make
-cd .. && rm -rf page
+cd website && make && cd .. && rm -rf website
 
 date
diff -r a4e163c7ed9c -r f9f2e1643593 Admin/makedist
--- a/Admin/makedist	Mon Jun 06 14:11:05 2005 +0200
+++ b/Admin/makedist	Mon Jun 06 14:12:07 2005 +0200
@@ -161,11 +161,20 @@
 
 cd "$DISTBASE/$DISTNAME" || fail "Something is wrong: dist directory doesn't exist!"
 
-cp -R Admin/page ..
-cp Distribution/doc/Contents ../page
-cp Distribution/lib/logo/isabelle.gif ../page/main-content
-cp Distribution/lib/logo/isabelle.gif ../page/dist-content
-echo "$DISTNAME" > ../page/DISTNAME
+#~ # old site framework
+#~ cp -R Admin/page ..
+#~ cp Distribution/doc/Contents ../page
+#~ cp Distribution/lib/logo/isabelle.gif ../page/main-content
+#~ cp Distribution/lib/logo/isabelle.gif ../page/dist-content
+#~ echo "$DISTNAME" > ../page/DISTNAME
+# new site framework
+cp -R Admin/website ..
+mkdir -p ../website/conf
+cat > ../website/conf/distname.mak <<EOF
+# this is a generated file - do not edit unless you know what you are doing
+
+DISTNAME=$DISTNAME
+EOF
 
 MOVE=$($FIND Doc \( -type f -a -not -type l -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
 mv -f $MOVE Distribution/doc