equal
deleted
inserted
replaced
22 |
22 |
23 #GNU tar (notably on Mac OS X) |
23 #GNU tar (notably on Mac OS X) |
24 if type -p gnutar >/dev/null |
24 if type -p gnutar >/dev/null |
25 then |
25 then |
26 function tar() { gnutar "$@"; } |
26 function tar() { gnutar "$@"; } |
|
27 export -f tar |
|
28 elif type -p gtar >/dev/null |
|
29 then |
|
30 function tar() { gtar "$@"; } |
27 export -f tar |
31 export -f tar |
28 fi |
32 fi |
29 |
33 |
30 #OCaml management via OPAM |
34 #OCaml management via OPAM |
31 function isabelle_opam() |
35 function isabelle_opam() |