diff -r 28a582aa25dd -r a117c076aa22 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Sun Sep 12 22:31:51 2021 +0200
+++ b/src/Pure/ML/ml_console.scala	Mon Sep 13 11:52:32 2021 +0200
@@ -60,7 +60,7 @@
           progress.interrupt_handler {
             Build.build_logic(options, logic, build_heap = true, progress = progress, dirs = dirs)
           }
-        if (rc != 0) sys.exit(rc)
+        if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
 
       // process loop
@@ -77,7 +77,7 @@
       POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join()
         val rc = process.join()
-        if (rc != 0) sys.exit(rc)
+        if (rc != Process_Result.RC.ok) sys.exit(rc)
       }
     }
   }