equal
deleted
inserted
replaced
1 # -*- shell-script -*- :mode=shellscript: |
1 # -*- shell-script -*- :mode=shellscript: |
2 |
2 |
3 TPTP_HOME="$COMPONENT" |
3 TPTP_HOME="$COMPONENT" |
4 |
4 |
5 ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools" |
5 ISABELLE_TOOLS="$ISABELLE_TOOLS:$TPTP_HOME/lib/Tools" |