find empty dirs up to depth 5;
authorwenzelm
Sun, 05 Jun 2005 23:07:24 +0200
changeset 16286 550d113ccd8f
parent 16285 75954ae8b247
child 16287 7a03b4b4df67
find empty dirs up to depth 5; tuned move of generated doc files; rm -f TODO;
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