lib/scripts/getfunctions
changeset 72162 5894859c5c84
parent 71736 a2afc7ed2c68
child 72465 de11c745ebbc
equal deleted inserted replaced
72161:cf443b24ad90 72162:5894859c5c84
   157     fi
   157     fi
   158   done
   158   done
   159   export ISABELLE_SCALA_SERVICES
   159   export ISABELLE_SCALA_SERVICES
   160 }
   160 }
   161 export -f isabelle_scala_service
   161 export -f isabelle_scala_service
       
   162 
       
   163 #Special directories
       
   164 function isabelle_directory ()
       
   165 {
       
   166   local X=""
       
   167   for X in "$@"
       
   168   do
       
   169     if [ -z "$ISABELLE_DIRECTORIES" ]; then
       
   170       ISABELLE_DIRECTORIES="$X"
       
   171     else
       
   172       ISABELLE_DIRECTORIES="$ISABELLE_DIRECTORIES:$X"
       
   173     fi
       
   174   done
       
   175   export ISABELLE_DIRECTORIES
       
   176 }
       
   177 export -f isabelle_directory
   162 
   178 
   163 #administrative build
   179 #administrative build
   164 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   180 if [ -e "$ISABELLE_HOME/Admin/build" ]; then
   165   function isabelle_admin_build ()
   181   function isabelle_admin_build ()
   166   {
   182   {