# HG changeset patch
# User wenzelm
# Date 1313060723 -7200
# Node ID aefbb5cc890885ec50ed9fea03f77454200759a9
# Parent  a07748619f53273711c9e1675b0e124cacabbf26
minimal script to run raw Poly/ML with concurrency library;

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"
+