# HG changeset patch
# User wenzelm
# Date 969985441 -7200
# Node ID 36d1218b58f4030e5b34464a8a63c534fae2c16d
# Parent  39f94bf02706988fc1586fe58d1154ba7ed8f8a7
FAKE_BUILD="";

diff -r 39f94bf02706 -r 36d1218b58f4 Admin/makebin
--- 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$$"