# HG changeset patch
# User wenzelm
# Date 1656422585 -7200
# Node ID e3aa7214eb1ab6eaa0a2d86028a3caef78d9943d
# Parent  11e233ba53c8eb6260c36dd8506d826f3cf19a2f
prefer Scala operations;

diff -r 11e233ba53c8 -r e3aa7214eb1a 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