equal
deleted
inserted
replaced
22 if type -p gnutar >/dev/null |
22 if type -p gnutar >/dev/null |
23 then |
23 then |
24 function tar() { gnutar "$@"; } |
24 function tar() { gnutar "$@"; } |
25 export -f tar |
25 export -f tar |
26 fi |
26 fi |
|
27 |
|
28 #OCaml management via OPAM |
|
29 function isabelle_opam() |
|
30 { |
|
31 if [ -z "$ISABELLE_OPAM" ]; then |
|
32 echo "Unknown ISABELLE_OPAM -- OCaml management tools unavailable" >&2 |
|
33 return 127 |
|
34 else |
|
35 env OPAMROOT="$ISABELLE_OPAM_ROOT" "$ISABELLE_OPAM" "$@" |
|
36 fi |
|
37 } |
|
38 export -f isabelle_opam |
27 |
39 |
28 #robust invocation via ISABELLE_JDK_HOME |
40 #robust invocation via ISABELLE_JDK_HOME |
29 function isabelle_jdk () |
41 function isabelle_jdk () |
30 { |
42 { |
31 if [ -z "$ISABELLE_JDK_HOME" ]; then |
43 if [ -z "$ISABELLE_JDK_HOME" ]; then |