diff -r 842b5e7dcac8 -r 7b396ef36af6 src/Pure/System/options.scala --- a/src/Pure/System/options.scala Sat Jul 27 16:59:25 2013 +0200 +++ b/src/Pure/System/options.scala Sat Jul 27 17:34:56 2013 +0200 @@ -142,9 +142,12 @@ if (get_option != "") java.lang.System.out.println(options.check_name(get_option).value) - else if (export_file != "") + + if (export_file != "") File.write(Path.explode(export_file), YXML.string_of_body(options.encode)) - else java.lang.System.out.println(options.print) + + if (get_option == "" && export_file == "") + java.lang.System.out.println(options.print) 0 case _ => error("Bad arguments:\n" + cat_lines(args))