practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
authorwenzelm
Wed, 14 May 2014 12:15:07 +0200
changeset 56959 0953208a32c7
parent 56958 b2c2f74d1c93
child 56960 e7bf30290627
practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
Admin/polyml/CHECKLIST
Admin/polyml/polyml
--- 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" "$@"
-