configure Admin as component, with its own lib/Tools;
authorwenzelm
Wed Aug 08 10:56:37 2012 +0200 (2012-08-08)
changeset 48725e852f4d6af80
parent 48724 e6e1b436caf0
child 48726 0bc8d90d2717
configure Admin as component, with its own lib/Tools;
Admin/etc/settings
lib/scripts/getsettings
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/Admin/etc/settings	Wed Aug 08 10:56:37 2012 +0200
     1.3 @@ -0,0 +1,3 @@
     1.4 +# -*- shell-script -*- :mode=shellscript:
     1.5 +
     1.6 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     2.1 --- a/lib/scripts/getsettings	Wed Aug 08 10:40:52 2012 +0200
     2.2 +++ b/lib/scripts/getsettings	Wed Aug 08 10:56:37 2012 +0200
     2.3 @@ -198,6 +198,7 @@
     2.4  #main components
     2.5  init_component "$ISABELLE_HOME"
     2.6  [ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src"
     2.7 +[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin"
     2.8  [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER"
     2.9  
    2.10  #ML system identifier