--- a/Admin/makebin Tue Sep 26 18:23:29 2000 +0200 +++ b/Admin/makebin Tue Sep 26 18:24:01 2000 +0200 @@ -7,7 +7,7 @@ ## global settings -FAKE_BUILD="true" +FAKE_BUILD="" DISTBASE=~/tmp/isadist TMP="/tmp/isabelle-makebin$$"