diff -r 38804edb8cf5 -r 34e56a6668ba lib/scripts/run-polyml
--- 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"