# HG changeset patch
# User wenzelm
# Date 1116317982 -7200
# Node ID c0c4088edccf0b54bd6e8777a0d46f804dbe5a0f
# Parent  b8855873d2346a8801ebd55ffb03ee6528dc046f
removed THIS_IS_ISABELLE_ADMIN;

diff -r b8855873d234 -r c0c4088edccf Admin/makebin
--- 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