# HG changeset patch
# User wenzelm
# Date 1118005644 -7200
# Node ID 550d113ccd8ffd8ab0f02b35ed28a88dd092918e
# Parent  75954ae8b24770fcac081e6f97bdb7dc85d444e3
find empty dirs up to depth 5;
tuned move of generated doc files;
rm -f TODO;

diff -r 75954ae8b247 -r 550d113ccd8f Admin/makedist
--- 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