misc tuning and clarification (NB: settings are already local for named snapshots/releases);
authorwenzelm
Sun, 11 Sep 2011 14:58:52 +0200
changeset 44877 a4761fc03ee7
parent 44876 243e2a413787
child 44878 1cbe20966cdb
misc tuning and clarification (NB: settings are already local for named snapshots/releases);
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"