--- a/Admin/makebin Mon Sep 26 20:12:51 2005 +0200 +++ b/Admin/makebin Mon Sep 26 20:51:57 2005 +0200 @@ -7,7 +7,6 @@ ## global settings -DISTBASE=~/tmp/isadist TMP="/var/tmp/isabelle-makebin$$" TAR=tar