# HG changeset patch
# User kleing
# Date 1152136282 -7200
# Node ID 283dfd5bd36b95e68b9432eda4c3750eb3118df2
# Parent  5419a71d0baae880f3cc2227fddd97f010836ca9
make sure $DISTPREFIX exists before calling makedist

diff -r 5419a71d0baa -r 283dfd5bd36b Admin/isatest-makedist
--- a/Admin/isatest-makedist	Wed Jul 05 16:24:28 2006 +0200
+++ b/Admin/isatest-makedist	Wed Jul 05 23:51:22 2006 +0200
@@ -60,6 +60,7 @@
 rm -rf $HOME/isabelle-*
 
 echo "### building distribution"  >> $DISTLOG 2>&1
+mkdir -p $DISTPREFIX
 $MAKEDIST - >> $DISTLOG 2>&1
 
 if [ $? -ne 0 ]