# HG changeset patch
# User wenzelm
# Date 1400062507 -7200
# Node ID 0953208a32c7076f39711dabfe15d103622138fc
# Parent  b2c2f74d1c93299547bd9a6dd0d4b30ad7b5daa9
practically obsolete: plain "poly" should work, except for Linux without libgmp installed;

diff -r b2c2f74d1c93 -r 0953208a32c7 Admin/polyml/CHECKLIST
--- 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
 
diff -r b2c2f74d1c93 -r 0953208a32c7 Admin/polyml/polyml
--- 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" "$@"
-