--- a/Admin/polyml/polyi Fri Feb 09 11:14:13 2018 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-#!/usr/bin/env bash
-#
-# Portable Poly/ML command-line tool
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
-
-if type -p rlwrap > /dev/null
-then
- exec rlwrap "$THIS/poly" "$@"
-else
- exec "$THIS/poly" "$@"
-fi
--- a/Admin/polyml/settings Fri Feb 09 11:14:13 2018 +0100
+++ b/Admin/polyml/settings Fri Feb 09 11:47:18 2018 +0100
@@ -36,7 +36,7 @@
do
if [ -z "$ML_HOME" ]
then
- if "$POLYML_HOME/$PLATFORM/polyi" -v </dev/null >/dev/null 2>/dev/null
+ if "$POLYML_HOME/$PLATFORM/poly" -v </dev/null >/dev/null 2>/dev/null
then
# ML settings
--- a/src/Pure/Admin/build_polyml.scala Fri Feb 09 11:14:13 2018 +0100
+++ b/src/Pure/Admin/build_polyml.scala Fri Feb 09 11:47:18 2018 +0100
@@ -165,7 +165,7 @@
entry <- File.read_dir(dir)
} File.move(dir + Path.explode(entry), target)
- for (file <- "~~/Admin/polyml/polyi" :: info.copy_files ::: ldd_files ::: sha1_files)
+ for (file <- info.copy_files ::: ldd_files ::: sha1_files)
File.copy(Path.explode(file).expand_env(settings), target)