| author | wenzelm |
| Sat, 28 Nov 2020 16:25:29 +0100 | |
| changeset 72759 | bd5ee3148132 |
| 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 |