equal
deleted
inserted
replaced
19 function standard_path() { echo "$@"; } |
19 function standard_path() { echo "$@"; } |
20 fi |
20 fi |
21 export -f platform_path standard_path |
21 export -f platform_path standard_path |
22 |
22 |
23 #GNU tar (notably on macOS) |
23 #GNU tar (notably on macOS) |
24 if type -p gnutar >/dev/null |
24 function tar() { "${ISABELLE_TAR:-false}" "$@"; } |
25 then |
25 export -f tar |
26 function tar() { gnutar "$@"; } |
|
27 export -f tar |
|
28 elif type -p gtar >/dev/null |
|
29 then |
|
30 function tar() { gtar "$@"; } |
|
31 export -f tar |
|
32 fi |
|
33 |
26 |
34 #OCaml management via OPAM |
27 #OCaml management via OPAM |
35 function isabelle_opam () |
28 function isabelle_opam () |
36 { |
29 { |
37 if [ -z "$ISABELLE_OPAM" ]; then |
30 if [ -z "$ISABELLE_OPAM" ]; then |