--- a/Admin/makebin Tue May 17 10:08:24 2005 +0200 +++ b/Admin/makebin Tue May 17 10:19:42 2005 +0200 @@ -14,7 +14,6 @@ type -path gtar >/dev/null && TAR=gtar export THIS_IS_ISABELLE_BUILD=true -export THIS_IS_ISABELLE_ADMIN=true ## diagnostics