# HG changeset patch
# User wenzelm
# Date 862589941 -7200
# Node ID 808681776bf79e61886bf8933cfbcc82da61d9ea
# Parent  a31170b673673b7851ec921da8288ac898d1af82
-P option (prune empty dirs);

diff -r a31170b67367 -r 808681776bf7 Admin/makedist
--- 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