practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
--- a/Admin/polyml/CHECKLIST Wed May 14 12:00:18 2014 +0200
+++ b/Admin/polyml/CHECKLIST Wed May 14 12:15:07 2014 +0200
@@ -11,7 +11,5 @@
* include sha1 source and binary for each platform
-* copy polyml script for each platform
-
* linux: include copy of libgmp.so with symlinks from build host
--- a/Admin/polyml/polyml Wed May 14 12:00:18 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-#
-# Minimal Poly/ML startup script
-
-THIS="$(cd "$(dirname "$0")"; pwd)"
-
-export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH"
-export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
-
-exec "$THIS/poly" "$@"
-