# HG changeset patch
# User wenzelm
# Date 1289832118 -3600
# Node ID 34e56a6668ba3af8d1c71f331f305fd3c79bce44
# Parent  38804edb8cf561bb689ffe91dc6d8d79eae972fc
tuned error messages;

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"
 
diff -r 38804edb8cf5 -r 34e56a6668ba lib/scripts/run-smlnj
--- a/lib/scripts/run-smlnj	Mon Nov 15 14:59:53 2010 +0100
+++ b/lib/scripts/run-smlnj	Mon Nov 15 15:41:58 2010 +0100
@@ -9,19 +9,20 @@
 
 ## 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_mlhome_file()
 {
-  if [ ! -f "$1" ]; then
-    echo "Unable to locate $1" >&2
-    echo "Please check your ML_HOME setting!" >&2
-    exit 2
-  fi
+  [ ! -f "$1" ] && fail "Unable to locate \"$1\""
 }
 
 function check_heap_file()
@@ -38,6 +39,8 @@
 
 ## compiler binaries
 
+[ -z "$ML_HOME" ] && fail "Missing ML installation (ML_HOME)"
+
 SML="$ML_HOME/sml"
 ARCH_N_OPSYS="$ML_HOME/.arch-n-opsys"