# HG changeset patch
# User wenzelm
# Date 1204827679 -3600
# Node ID 79c8d7277f33287a8194eb44a3e533542b8464e9
# Parent  278f47ae70d1b907b3b40a829edd7e56987ae768
removed obsolete THIS_IS_ISABELLE_BUILD/MAKEBIN feature;

diff -r 278f47ae70d1 -r 79c8d7277f33 Admin/makebin
--- a/Admin/makebin	Wed Mar 05 22:58:13 2008 +0100
+++ b/Admin/makebin	Thu Mar 06 19:21:19 2008 +0100
@@ -12,9 +12,6 @@
 TAR=tar
 type -path gtar >/dev/null && TAR=gtar
 
-export THIS_IS_ISABELLE_BUILD=true
-export THIS_IS_ISABELLE_MAKEBIN=true
-
 
 ## diagnostics