changeset 56959 | 0953208a32c7 |
parent 56958 | b2c2f74d1c93 |
child 56960 | e7bf30290627 |
--- 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" "$@" -