-P option (prune empty dirs);

--- a/Admin/makedist	Fri May 02 16:41:35 1997 +0200
+++ b/Admin/makedist	Fri May 02 18:19:01 1997 +0200
@@ -100,7 +100,7 @@
 cd $DISTBASE
 
 export CVSROOT
-cvs -f -q $EXPORT -d $DISTNAME isabelle
+cvs -f -q $EXPORT -P -d $DISTNAME isabelle
 
 
 # make docs
@@ -118,8 +118,9 @@
 
 find . -name CVS -exec rm -rf {} \;
 
+mkdir -p Tools/8bit/bin    #FIXME tmp
 find Doc -name \*.dvi -exec mv {} Distribution/doc \;
-rm -rf Admin Doc examples Modal LK HOLCF/explicit_domains
+rm -rf Admin Doc
 
 mkdir src
 mv $LOGICS src