# HG changeset patch # User wenzelm # Date 1678538278 -3600 # Node ID 44f7b76d110672dcb338da6aee0532c7e8f54909 # Parent 3e235fab64db357a344b5129213ef8b35d31df89 tuned; diff -r 3e235fab64db -r 44f7b76d1106 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Mar 11 13:31:16 2023 +0100 +++ b/src/Pure/System/options.scala Sat Mar 11 13:37:58 2023 +0100 @@ -219,20 +219,24 @@ val options = { val options0 = Options.init() val options1 = - if (build_options) + if (build_options) { Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")).foldLeft(options0)(_ + _) + } else options0 more_options.foldLeft(options1)(_ + _) } - if (get_option != "") + if (get_option != "") { Output.writeln(options.check_name(get_option).value, stdout = true) + } - if (export_file != "") + if (export_file != "") { File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) + } - if (get_option == "" && export_file == "") + if (get_option == "" && export_file == "") { Output.writeln(options.print, stdout = true) + } }) }