diff -r 3f02bc5a5a03 -r c1bc38327bc2 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Mon Mar 30 19:39:11 2020 +0200
+++ b/src/Pure/ML/ml_console.scala	Mon Mar 30 19:50:01 2020 +0200
@@ -81,7 +81,9 @@
         rc
       }
       tty_loop.join
-      process_result.join
+
+      val rc = process_result.join
+      if (rc != 0) sys.exit(rc)
     }
   }
 }