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