--- 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