--- a/lib/scripts/run-polyml Mon Nov 15 14:59:53 2010 +0100
+++ b/lib/scripts/run-polyml Mon Nov 15 15:41:58 2010 +0100
@@ -9,24 +9,27 @@
## diagnostics
+function fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
function fail_out()
{
- echo "Unable to create output heap file: \"$OUTFILE\"" >&2
- exit 2
+ fail "Unable to create output heap file: \"$OUTFILE\""
}
function check_file()
{
- if [ ! -f "$1" ]; then
- echo "Unable to locate $1" >&2
- echo "Please check your ML system settings!" >&2
- exit 2
- fi
+ [ ! -f "$1" ] && fail "Unable to locate \"$1\""
}
## compiler executables and libraries
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
POLY="$ML_HOME/poly"
check_file "$POLY"