--- 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