changeset 74306 | a117c076aa22 |
parent 74037 | c13198575f75 |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/System/getopts.scala Sun Sep 12 22:31:51 2021 +0200 +++ b/src/Pure/System/getopts.scala Mon Sep 13 11:52:32 2021 +0200 @@ -33,7 +33,7 @@ def usage(): Nothing = { Output.writeln(usage_text, stdout = true) - sys.exit(1) + sys.exit(Process_Result.RC.error) } private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)