src/Tools/Setup/src/Exn.java
changeset 74067 0b1462ce5fda
parent 74031 09821ca262d3
child 74068 62e4ec8cff38
--- a/src/Tools/Setup/src/Exn.java	Sun Jul 25 16:38:16 2021 +0200
+++ b/src/Tools/Setup/src/Exn.java	Mon Jul 26 13:04:55 2021 +0200
@@ -27,11 +27,9 @@
         return found_interrupt;
     }
 
-    public static int INTERRUPT_RETURN_CODE = 130;
-
     public static int return_code(Throwable exn, int rc)
     {
-        return is_interrupt(exn) ? INTERRUPT_RETURN_CODE : rc;
+        return is_interrupt(exn) ? 130 : rc;
     }