src/Tools/Setup/src/Setup.java
changeset 74068 62e4ec8cff38
parent 74061 203dfa8bc0fc
--- a/src/Tools/Setup/src/Setup.java	Mon Jul 26 13:04:55 2021 +0200
+++ b/src/Tools/Setup/src/Setup.java	Mon Jul 26 13:12:22 2021 +0200
@@ -59,7 +59,7 @@
         }
         catch (Throwable exn) {
             echo_err(Exn.print_error(exn));
-            System.exit(Exn.return_code(exn, 2));
+            System.exit(Exn.failure_rc(exn));
         }
     }
 }