diff -r a07748619f53 -r aefbb5cc8908 Admin/polyml/future/run
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/polyml/future/run	Thu Aug 11 13:05:23 2011 +0200
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+POLY="${1:-poly}"
+
+THIS="$(cd $(dirname "$0"); pwd)"
+
+cd "$THIS/../../../src/Pure"
+echo "use \"../../Admin/polyml/future/ROOT.ML\";"
+env ML_SYSTEM=dummy ML_PLATFORM=dummy "$POLY"
+