| author | wenzelm | 
| Sun, 14 Jan 2018 15:06:27 +0100 | |
| changeset 67426 | 6311cf9dc943 | 
| parent 63229 | f951c624c1a1 | 
| child 67580 | eb64467e8bcf | 
| permissions | -rwxr-xr-x | 
| 33833 | 1 | #!/usr/bin/env bash | 
| 2 | # | |
| 63229 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 3 | # Portable Poly/ML command-line tool | 
| 33833 | 4 | |
| 5 | THIS="$(cd "$(dirname "$0")"; pwd)" | |
| 6 | ||
| 7 | export LD_LIBRARY_PATH="$THIS:$LD_LIBRARY_PATH" | |
| 8 | export DYLD_LIBRARY_PATH="$THIS:$DYLD_LIBRARY_PATH" | |
| 9 | ||
| 63229 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 10 | if type -p rlwrap > /dev/null | 
| 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 11 | then | 
| 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 12 | exec rlwrap "$THIS/poly" "$@" | 
| 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 13 | else | 
| 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 14 | exec "$THIS/poly" "$@" | 
| 
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
 wenzelm parents: 
60983diff
changeset | 15 | fi |