# HG changeset patch
# User wenzelm
# Date 1332104940 -3600
# Node ID 1d8601c642cce08a27783450ae8fb09d20da65c4
# Parent  ceba98191816134ec338bea33881f6b62831260e
more robust bash interpolation;

diff -r ceba98191816 -r 1d8601c642cc Admin/makedist
--- a/Admin/makedist	Sun Mar 18 22:06:37 2012 +0100
+++ b/Admin/makedist	Sun Mar 18 22:09:00 2012 +0100
@@ -6,7 +6,7 @@
 
 REPOS_NAME="isabelle"
 REPOS="${REPOS:-http://isabelle.in.tum.de/repos/${REPOS_NAME}}"
-DISTPREFIX="${DISTPREFIX:-~/tmp/isadist}"
+DISTPREFIX="${DISTPREFIX:-$HOME/tmp/isadist}"
 
 umask 022