author | wenzelm |
Fri, 02 Sep 2016 16:23:02 +0200 | |
changeset 63773 | d1a5d10affc0 |
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:
60983
diff
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:
60983
diff
changeset
|
10 |
if type -p rlwrap > /dev/null |
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
wenzelm
parents:
60983
diff
changeset
|
11 |
then |
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
wenzelm
parents:
60983
diff
changeset
|
12 |
exec rlwrap "$THIS/poly" "$@" |
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
wenzelm
parents:
60983
diff
changeset
|
13 |
else |
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
wenzelm
parents:
60983
diff
changeset
|
14 |
exec "$THIS/poly" "$@" |
f951c624c1a1
updated to recent changes of Poly/ML directory layout;
wenzelm
parents:
60983
diff
changeset
|
15 |
fi |