# HG changeset patch
# User wenzelm
# Date 1127760717 -7200
# Node ID 94bbe14c088e8079a9207d557618549c1a2fb1d0
# Parent  b1019337c857913d249e76caeb5076a17541cf6a
tuned;

diff -r b1019337c857 -r 94bbe14c088e Admin/makebin
--- 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