# HG changeset patch
# User wenzelm
# Date 939299461 -7200
# Node ID 7a8e91b8c100a6488b5228924555c3ad0f6ba5c7
# Parent  099742c562aa009fb35934751610efae32a5b007
delete Tools;

diff -r 099742c562aa -r 7a8e91b8c100 Admin/makedist
--- a/Admin/makedist	Thu Oct 07 12:52:23 1999 +0200
+++ b/Admin/makedist	Thu Oct 07 14:31:01 1999 +0200
@@ -130,7 +130,7 @@
 mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps
 cp Admin/index.html $DISTBASE
-rm -rf Admin Doc
+rm -rf Admin Doc Tools
 
 mkdir src contrib
 mv $LOGICS src