diff -r fa4f45fa4666 -r 46def28153d6 lib/scripts/run-polyml
--- a/lib/scripts/run-polyml	Thu Aug 31 14:11:04 2000 +0200
+++ b/lib/scripts/run-polyml	Thu Aug 31 17:25:52 2000 +0200
@@ -35,6 +35,16 @@
 check_mlhome_file "$DISCGARB"
 
 
+case "$ML_SYSTEM" in
+  polyml-4.*)
+    EXIT="fun exit 0 = (OS.Process.exit OS.Process.success): unit | exit _ = OS.Process.exit OS.Process.failure;"
+    ;;
+  *)
+    EXIT="val exit = PolyML.exit;"
+    ;;
+esac
+
+
 ## prepare databases
 
 COPYDB=true
@@ -42,8 +52,8 @@
 if [ -z "$INFILE" ]; then
   INFILE="$ML_HOME/ML_dbase"
   check_mlhome_file "$INFILE"
-  MLTEXT="val use = PolyML.use; val exit = PolyML.exit; $MLTEXT"
   COPYDB=""
+  MLTEXT="val use = PolyML.use; $EXIT $MLTEXT"
 fi
 
 if [ -z "$OUTFILE" ]; then