diff -r d3c5195b7399 -r 725916b7dee5 lib/scripts/getsettings
--- a/lib/scripts/getsettings	Tue Jun 25 11:26:15 2013 +0200
+++ b/lib/scripts/getsettings	Tue Jun 25 11:41:16 2013 +0200
@@ -60,7 +60,8 @@
 unset BASH_ENV
 
 #shared library convenience
-function librarypath () {
+function librarypath ()
+{
   for X in "$@"
   do
     case "$ISABELLE_PLATFORM" in
@@ -85,7 +86,8 @@
 }
 
 #robust invocation via ISABELLE_JDK_HOME
-function isabelle_jdk () {
+function isabelle_jdk ()
+{
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
     return 127
@@ -96,7 +98,8 @@
 }
 
 #robust invocation via SCALA_HOME
-function isabelle_scala () {
+function isabelle_scala ()
+{
   if [ -z "$ISABELLE_JDK_HOME" ]; then
     echo "Unknown ISABELLE_JDK_HOME -- Java tools unavailable" >&2
     return 127
@@ -109,8 +112,19 @@
   fi
 }
 
+#administrative build
+if [ -e "$ISABELLE_HOME/Admin/build" ]; then
+  function isabelle_admin_build ()
+  {
+    "$ISABELLE_HOME/Admin/build" "$@"
+  }
+else
+  function isabelle_admin_build () { return 0; }
+fi
+
 #CLASSPATH convenience
-function classpath () {
+function classpath ()
+{
   for X in "$@"
   do
     if [ -z "$CLASSPATH" ]; then