--- a/lib/scripts/getfunctions Sun Mar 13 12:50:46 2016 +0100
+++ b/lib/scripts/getfunctions Sun Mar 13 13:04:50 2016 +0100
@@ -24,33 +24,6 @@
export -f tar
fi
-#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
-}
-export -f librarypath
-
#robust invocation via ISABELLE_JDK_HOME
function isabelle_jdk ()
{
--- a/src/Pure/System/isabelle_system.scala Sun Mar 13 12:50:46 2016 +0100
+++ b/src/Pure/System/isabelle_system.scala Sun Mar 13 13:04:50 2016 +0100
@@ -144,6 +144,16 @@
def cygwin_root(): String = getenv_strict("CYGWIN_ROOT")
+ def library_path(env: Map[String, String], elem: String): Map[String, String] =
+ if (Platform.is_windows) env
+ else {
+ val x = if (Platform.is_macos) "DYLD_LIBRARY_PATH" else "LD_LIBRARY_PATH"
+ env.getOrElse(x, "") match {
+ case "" => env + (x -> elem)
+ case y => env + (x -> (y + ":" + elem))
+ }
+ }
+
/** file-system operations **/
--- a/src/Pure/Tools/ml_process.scala Sun Mar 13 12:50:46 2016 +0100
+++ b/src/Pure/Tools/ml_process.scala Sun Mar 13 13:04:50 2016 +0100
@@ -98,9 +98,12 @@
(eval_heaps ::: eval_initial ::: eval_modes ::: eval_options ::: eval_secure ::: eval_process).
map(eval => List("--eval", eval)).flatten ::: args
- Bash.process(
- """librarypath "$ML_HOME"; exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
- cwd = cwd, env = env ++ env_options ++ env_tmp, redirect = redirect,
+ Bash.process("""exec "$ML_HOME/poly" -q """ + File.bash_args(bash_args),
+ cwd = cwd,
+ env =
+ Isabelle_System.library_path(env ++ env_options ++ env_tmp,
+ Isabelle_System.getenv_strict("ML_HOME")),
+ redirect = redirect,
cleanup = () =>
{
isabelle_process_options.delete