--- 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 ]