# HG changeset patch
# User wenzelm
# Date 1180785127 -7200
# Node ID 85612df29daa0822a6ea14f419a60d231588e3a4
# Parent  d47e2daac66573dfcc356ed0206062de8b4e678f
proper handling of Tools;

diff -r d47e2daac665 -r 85612df29daa Admin/makedist
--- a/Admin/makedist	Sat Jun 02 08:54:05 2007 +0200
+++ b/Admin/makedist	Sat Jun 02 13:52:07 2007 +0200
@@ -165,7 +165,7 @@
 MOVE=$($FIND Doc \( -type f -a -not -type l -a -not -name isabelle_isar.pdf -a -not -name pghead.pdf -a \( -name \*.dvi -o -name \*.eps -o -name \*.ps -o -name \*.pdf \) -a -print \) | grep -v 'gfx/.*pdf')
 mv -f $MOVE Distribution/doc
 rm Distribution/doc/Isa-logics.eps
-rm -rf Doc Tools
+rm -rf Doc
 
 mkdir src contrib
 mv $SRCS src