# HG changeset patch
# User wenzelm
# Date 967822649 -7200
# Node ID 63b195acdaaa3a5b329008ff4a8552cce747a87c
# Parent  32378f1c2f1765785275f753baffb0c1c3fb00c6
cleanup dist sources afterwards;
tmp version;

diff -r 32378f1c2f17 -r 63b195acdaaa Admin/makedist
--- a/Admin/makedist	Fri Sep 01 17:36:42 2000 +0200
+++ b/Admin/makedist	Fri Sep 01 17:37:29 2000 +0200
@@ -191,9 +191,23 @@
 gzip ${DISTNAME}_pdf.tar
 
 
+# cleanup dist
+
+mv $DISTNAME ${DISTNAME}-old
+mkdir $DISTNAME
+
+mv ${DISTNAME}-old/lib/logo/isabelle.gif .
+mv ${DISTNAME}-old/README.html ${DISTNAME}-old/INSTALL $DISTNAME
+mkdir $DISTNAME/doc && \
+  mv ${DISTNAME}-old/doc/*.pdf ${DISTNAME}-old/doc/Contents $DISTNAME/doc
+
+rm -rf ${DISTNAME}-old
+
+
 # prepare web pages
 
-$THIS/filesizes -norpm
+#FIXME
+#$THIS/filesizes -norpm
 
 
 # final note