# HG changeset patch
# User wenzelm
# Date 1315745932 -7200
# Node ID a4761fc03ee751cf82e47f6e9b01413452815caa
# Parent  243e2a4137870a86218346d15a1bed4f69635c08
misc tuning and clarification (NB: settings are already local for named snapshots/releases);

diff -r 243e2a413787 -r a4761fc03ee7 Admin/makebin
--- a/Admin/makebin	Sun Sep 11 14:42:15 2011 +0200
+++ b/Admin/makebin	Sun Sep 11 14:58:52 2011 +0200
@@ -7,8 +7,6 @@
 
 TMP="/var/tmp/isabelle-makebin$$"
 
-export THIS_IS_ISABELLE_MAKEBIN=true
-
 
 ## diagnostics
 
@@ -40,7 +38,7 @@
 
 DO_LIBRARY=""
 
-while getopts "ln" OPT
+while getopts "l" OPT
 do
   case "$OPT" in
     l)
@@ -91,8 +89,6 @@
 fi
 
 ISABELLE_HOME_USER=$(./bin/isabelle getenv -b ISABELLE_HOME_USER)
-[ -f "$ISABELLE_HOME_USER/etc/settings" ] && \
-  echo "### WARNING!  Personal Isabelle settings present. " >&2
 
 COMPILER=$(./bin/isabelle getenv -b ML_IDENTIFIER)
 PLATFORM=$(./bin/isabelle getenv -b ML_PLATFORM)
@@ -119,5 +115,4 @@
 
 
 # clean up
-cd /tmp
 rm -rf "$TMP"