changeset 8223 | 960ca167cfc5 |
parent 8134 | ceedd1a8bad6 |
child 9287 | c406d0af9368 |
8222:55fed562d8ed | 8223:960ca167cfc5 |
---|---|
56 fi |
56 fi |
57 fi |
57 fi |
58 |
58 |
59 make main |
59 make main |
60 |
60 |
61 mkdir -p $TARGET |
|
62 chgrp isabelle $TARGET |
|
63 chmod 775 $TARGET |
|
64 |
|
65 for FILE in $FILES; do |
61 for FILE in $FILES; do |
66 cp $PREFIX/$FILE $TARGET |
62 cp -f $PREFIX/$FILE $TARGET |
67 done |
63 done |
68 |
64 |
69 cd $TARGET |
65 chmod g=u $TARGET/* |
70 echo You should find the Isabelle pages in `pwd` |
66 |
67 ( cd $TARGET; echo -e "\nYou should find the Isabelle pages in $PWD"; ) |