--- a/Admin/makedist Sun Jun 05 21:32:37 2005 +0200
+++ b/Admin/makedist Sun Jun 05 23:07:24 2005 +0200
@@ -131,6 +131,8 @@
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
+$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
+$FIND . "(" -type d -a -empty ")" -print | xargs rm -rf
# build docs
@@ -165,7 +167,7 @@
cp Distribution/lib/logo/isabelle.gif ../page/dist-content
echo "$DISTNAME" > ../page/DISTNAME
-MOVE=$($FIND Doc \( -type f -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
+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
rm Distribution/doc/Isa-logics.eps
rm -rf Doc Tools
@@ -201,6 +203,7 @@
( cd src; ../Admin/maketags; )
rm -rf Admin
+rm -f TODO
# create archive