# HG changeset patch
# User wenzelm
# Date 1212183221 -7200
# Node ID 8c558af86e21e17f41a626d7d0c2cdeae2c32fe0
# Parent  0006d6a6d21d061821300aefa3e0e9a0c99bb7ea
THIS_IS_ISABELLE_MAKEBIN is back;

diff -r 0006d6a6d21d -r 8c558af86e21 Admin/makebin
--- a/Admin/makebin	Fri May 30 23:26:51 2008 +0200
+++ b/Admin/makebin	Fri May 30 23:33:41 2008 +0200
@@ -12,6 +12,8 @@
 TAR=tar
 type -path gtar >/dev/null && TAR=gtar
 
+export THIS_IS_ISABELLE_MAKEBIN=true
+
 
 ## diagnostics