# HG changeset patch
# User wenzelm
# Date 1235731563 -3600
# Node ID 45cf6c04846e7275689fe22dc3d2652165f601c0
# Parent  58388314ccc8e20405d003e946b4149e6d2b85fc
tuned;

diff -r 58388314ccc8 -r 45cf6c04846e Admin/makedist
--- a/Admin/makedist	Fri Feb 27 11:43:24 2009 +0100
+++ b/Admin/makedist	Fri Feb 27 11:46:03 2009 +0100
@@ -156,7 +156,7 @@
 rm doc/codegen_process.pdf
 rm -rf doc-src
 
-mkdir contrib
+mkdir -p contrib
 
 cp doc/isabelle*.eps lib/logo