Admin/etc/settings
changeset 59105 976e73e11d9a
parent 49740 e852f4d6af80
equal deleted inserted replaced
59104:09a9b04605e5 59105:976e73e11d9a
     1 # -*- shell-script -*- :mode=shellscript:
       
     2 
       
     3 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"