prefer Scala operations;
authorwenzelm
Tue, 28 Jun 2022 15:23:05 +0200
changeset 75630 e3aa7214eb1a
parent 75629 11e233ba53c8
child 75631 809c37bfd823
prefer Scala operations;
src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Tue Jun 28 15:17:47 2022 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Tue Jun 28 15:23:05 2022 +0200
@@ -181,6 +181,6 @@
 
     val post_result = config.post_hook(results)
 
-    System.exit(List(pre_result.rc, results.rc, post_result.rc).max)
+    sys.exit(List(pre_result.rc, results.rc, post_result.rc).max)
   }
 }
\ No newline at end of file