practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
authorwenzelm
Wed May 14 12:15:07 2014 +0200 (2014-05-14)
changeset 569590953208a32c7
parent 56958 b2c2f74d1c93
child 56960 e7bf30290627
practically obsolete: plain "poly" should work, except for Linux without libgmp installed;
Admin/polyml/CHECKLIST
Admin/polyml/polyml
     1.1 --- a/Admin/polyml/CHECKLIST	Wed May 14 12:00:18 2014 +0200
     1.2 +++ b/Admin/polyml/CHECKLIST	Wed May 14 12:15:07 2014 +0200
     1.3 @@ -11,7 +11,5 @@
     1.4  
     1.5  * include sha1 source and binary for each platform
     1.6  
     1.7 -* copy polyml script for each platform
     1.8 -
     1.9  * linux: include copy of libgmp.so with symlinks from build host
    1.10  
     2.1 --- a/Admin/polyml/polyml	Wed May 14 12:00:18 2014 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,11 +0,0 @@
     2.4 -#!/usr/bin/env bash
     2.5 -#
     2.6 -# Minimal Poly/ML startup script
     2.7 -
     2.8 -THIS="$(cd "$(dirname "$0")"; pwd)"
     2.9 -
    2.10 -export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH"
    2.11 -export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH"
    2.12 -
    2.13 -exec "$THIS/poly" "$@"
    2.14 -