author | wenzelm |
Wed, 02 May 2012 22:05:59 +0200 | |
changeset 47887 | 4e9c06c194d9 |
parent 44155 | ae2906662eec |
permissions | -rwxr-xr-x |
44153
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
1 |
#!/bin/bash |
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
2 |
|
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
3 |
POLY="${1:-poly}" |
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
4 |
|
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
5 |
THIS="$(cd $(dirname "$0"); pwd)" |
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
6 |
|
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
7 |
cd "$THIS/../../../src/Pure" |
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
8 |
echo "use \"../../Admin/polyml/future/ROOT.ML\";" |
44155 | 9 |
exec "$POLY" |
44153
aefbb5cc8908
minimal script to run raw Poly/ML with concurrency library;
wenzelm
parents:
diff
changeset
|
10 |