1 #!/bin/bash
2
3 POLY="${1:-poly}"
4
5 THIS="$(cd $(dirname "$0"); pwd)"
6
7 cd "$THIS/../../../src/Pure"
8 echo "use \"../../Admin/polyml/future/ROOT.ML\";"
9 env ML_SYSTEM=dummy ML_PLATFORM=dummy "$POLY"
10