# HG changeset patch
# User wenzelm
# Date 1359752293 -3600
# Node ID b0901f4a857a66c887b0a9c3f42f14b80643aef1
# Parent  f95817852bdd52958bbd6fcc7aca81e23e676a84# Parent  a25b899a649d5920c5f4cf4bfc2a73683bdb5206
merged

diff -r f95817852bdd -r b0901f4a857a Admin/lib/Tools/makedist
--- a/Admin/lib/Tools/makedist	Fri Feb 01 21:58:00 2013 +0100
+++ b/Admin/lib/Tools/makedist	Fri Feb 01 21:58:13 2013 +0100
@@ -106,6 +106,7 @@
   DISTVERSION="$DISTNAME: $DISTDATE"
 fi
 
+DISTPREFIX="$(cd "$DISTPREFIX"; pwd)"
 DISTBASE="$DISTPREFIX/dist-$DISTNAME"
 mkdir -p "$DISTBASE" || fail "Unable to create distribution base dir \"$DISTBASE\""