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