added librarypath: shared library convenience in bash, keeping LD_LIBRARY_PATH and DYLD_LIBRARY_PATH separate;
--- a/lib/scripts/getsettings Wed Jan 19 15:22:35 2011 +0100
+++ b/lib/scripts/getsettings Wed Jan 19 21:00:16 2011 +0100
@@ -63,6 +63,31 @@
fi
HOME_JVM="$HOME"
+#shared library convenience
+function librarypath () {
+ for X in "$@"
+ do
+ case "$ISABELLE_PLATFORM" in
+ *-darwin)
+ if [ -z "$DYLD_LIBRARY_PATH" ]; then
+ DYLD_LIBRARY_PATH="$X"
+ else
+ DYLD_LIBRARY_PATH="$X:$DYLD_LIBRARY_PATH"
+ fi
+ export DYLD_LIBRARY_PATH
+ ;;
+ *)
+ if [ -z "$LD_LIBRARY_PATH" ]; then
+ LD_LIBRARY_PATH="$X"
+ else
+ LD_LIBRARY_PATH="$X:$LD_LIBRARY_PATH"
+ fi
+ export LD_LIBRARY_PATH
+ ;;
+ esac
+ done
+}
+
#CLASSPATH convenience
function classpath () {
for X in "$@"
--- a/lib/scripts/run-polyml Wed Jan 19 15:22:35 2011 +0100
+++ b/lib/scripts/run-polyml Wed Jan 19 21:00:16 2011 +0100
@@ -39,8 +39,7 @@
POLYLIB="$ML_HOME"
fi
-export LD_LIBRARY_PATH="$POLYLIB:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$POLYLIB:$DYLD_LIBRARY_PATH"
+librarypath "$POLYLIB"
## prepare databases