--- 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