--- 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)
}
}
}