equal
deleted
inserted
replaced
25 #GNU tar (notably on Mac OS X) |
25 #GNU tar (notably on Mac OS X) |
26 if [ -x /usr/bin/gnutar ]; then |
26 if [ -x /usr/bin/gnutar ]; then |
27 function tar() { /usr/bin/gnutar "$@"; } |
27 function tar() { /usr/bin/gnutar "$@"; } |
28 export -f tar |
28 export -f tar |
29 fi |
29 fi |
30 |
|
31 #main executables |
|
32 function isabelle () |
|
33 { |
|
34 "$ISABELLE_TOOL" "$@" |
|
35 } |
|
36 export -f isabelle |
|
37 |
|
38 function isabelle_process () |
|
39 { |
|
40 "$ISABELLE_PROCESS" "$@" |
|
41 } |
|
42 export -f isabelle_process |
|
43 |
|
44 function isabelle_scala_script () |
|
45 { |
|
46 "$ISABELLE_SCALA_SCRIPT" "$@" |
|
47 } |
|
48 export -f isabelle_scala_script |
|
49 |
30 |
50 #shared library convenience |
31 #shared library convenience |
51 function librarypath () |
32 function librarypath () |
52 { |
33 { |
53 for X in "$@" |
34 for X in "$@" |