# HG changeset patch
# User wenzelm
# Date 950101934 -3600
# Node ID 960ca167cfc5f1594efc0e125c57357376970fc7
# Parent  55fed562d8ed91ecaaea4e402c5477d9f3d71573
tuned;

diff -r 55fed562d8ed -r 960ca167cfc5 Admin/makepage
--- a/Admin/makepage	Wed Feb 09 14:03:29 2000 +0100
+++ b/Admin/makepage	Wed Feb 09 14:12:14 2000 +0100
@@ -58,13 +58,10 @@
 
 make main
 
-mkdir -p $TARGET
-chgrp isabelle $TARGET
-chmod 775 $TARGET
-
 for FILE in $FILES; do
-    cp $PREFIX/$FILE $TARGET
+    cp -f $PREFIX/$FILE $TARGET
 done
 
-cd $TARGET
-echo You should find the Isabelle pages in `pwd`
\ No newline at end of file
+chmod g=u $TARGET/*
+
+( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; )