author | wenzelm |
Tue, 31 Mar 2015 22:31:05 +0200 | |
changeset 59886 | e0dc738eb08c |
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 |