# HG changeset patch
# User wenzelm
# Date 1014928257 -3600
# Node ID 9db054a402474dd9e404d33244ec2274be60ebf3
# Parent  6071200efbf688c7878beadfa025d7b40a5a85e3
export THIS_IS_ISABELLE_ADMIN=true;

diff -r 6071200efbf6 -r 9db054a40247 Admin/makebin
--- a/Admin/makebin	Thu Feb 28 21:30:26 2002 +0100
+++ b/Admin/makebin	Thu Feb 28 21:30:57 2002 +0100
@@ -14,6 +14,7 @@
 type -path gtar >/dev/null && TAR=gtar
 
 export THIS_IS_ISABELLE_BUILD=true
+export THIS_IS_ISABELLE_ADMIN=true
 
 
 ## diagnostics