equal
deleted
inserted
replaced
60 THIS_CYGWIN="$(jvmpath "/")" |
60 THIS_CYGWIN="$(jvmpath "/")" |
61 else |
61 else |
62 function jvmpath() { echo "$@"; } |
62 function jvmpath() { echo "$@"; } |
63 fi |
63 fi |
64 HOME_JVM="$HOME" |
64 HOME_JVM="$HOME" |
|
65 |
|
66 #shared library convenience |
|
67 function librarypath () { |
|
68 for X in "$@" |
|
69 do |
|
70 case "$ISABELLE_PLATFORM" in |
|
71 *-darwin) |
|
72 if [ -z "$DYLD_LIBRARY_PATH" ]; then |
|
73 DYLD_LIBRARY_PATH="$X" |
|
74 else |
|
75 DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH" |
|
76 fi |
|
77 export DYLD_LIBRARY_PATH |
|
78 ;; |
|
79 *) |
|
80 if [ -z "$LD_LIBRARY_PATH" ]; then |
|
81 LD_LIBRARY_PATH="$X" |
|
82 else |
|
83 LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH" |
|
84 fi |
|
85 export LD_LIBRARY_PATH |
|
86 ;; |
|
87 esac |
|
88 done |
|
89 } |
65 |
90 |
66 #CLASSPATH convenience |
91 #CLASSPATH convenience |
67 function classpath () { |
92 function classpath () { |
68 for X in "$@" |
93 for X in "$@" |
69 do |
94 do |