FAKE_BUILD="";
authorwenzelm
Tue Sep 26 18:24:01 2000 +0200 (2000-09-26)
changeset 1009036d1218b58f4
parent 10089 39f94bf02706
child 10091 43c1951a369c
FAKE_BUILD="";
Admin/makebin
     1.1 --- a/Admin/makebin	Tue Sep 26 18:23:29 2000 +0200
     1.2 +++ b/Admin/makebin	Tue Sep 26 18:24:01 2000 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  ## global settings
     1.6  
     1.7 -FAKE_BUILD="true"
     1.8 +FAKE_BUILD=""
     1.9  DISTBASE=~/tmp/isadist
    1.10  TMP="/tmp/isabelle-makebin$$"
    1.11