Admin/makedist
changeset 3099 808681776bf7
parent 3060 7c3564de392e
child 3169 c13e54126fcd
--- 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