# HG changeset patch # User wenzelm # Date 1344416197 -7200 # Node ID e852f4d6af8012d55bfec320793f1611c25ee7cc # Parent e6e1b436caf0a6ac30865d010df312ad68cb46ce configure Admin as component, with its own lib/Tools; diff -r e6e1b436caf0 -r e852f4d6af80 Admin/etc/settings --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Admin/etc/settings Wed Aug 08 10:56:37 2012 +0200 @@ -0,0 +1,3 @@ +# -*- shell-script -*- :mode=shellscript: + +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" diff -r e6e1b436caf0 -r e852f4d6af80 lib/scripts/getsettings --- a/lib/scripts/getsettings Wed Aug 08 10:40:52 2012 +0200 +++ b/lib/scripts/getsettings Wed Aug 08 10:56:37 2012 +0200 @@ -198,6 +198,7 @@ #main components init_component "$ISABELLE_HOME" [ -d "$ISABELLE_HOME/doc-src" ] && init_component "$ISABELLE_HOME/doc-src" +[ -d "$ISABELLE_HOME/Admin" ] && init_component "$ISABELLE_HOME/Admin" [ -d "$ISABELLE_HOME_USER" ] && init_component "$ISABELLE_HOME_USER" #ML system identifier