# HG changeset patch
# User wenzelm
# Date 970077071 -7200
# Node ID 1db5bd97f6a31b6e7e62cf5d81194a76a9ac3f93
# Parent  6cbe69107c18f7c92b5d28dde784bdb81c82bd1e
THIS_IS_ISABELLE_BUILD;

diff -r 6cbe69107c18 -r 1db5bd97f6a3 Admin/makebin
--- a/Admin/makebin	Wed Sep 27 19:39:50 2000 +0200
+++ b/Admin/makebin	Wed Sep 27 19:51:11 2000 +0200
@@ -14,6 +14,8 @@
 TAR=tar
 type -path gtar >/dev/null && TAR=gtar
 
+export THIS_IS_ISABELLE_BUILD=true
+
 
 ## diagnostics