src/Pure/System/options.scala
changeset 52737 7b396ef36af6
parent 52735 842b5e7dcac8
child 53336 b3bf6d72fea5
equal deleted inserted replaced
52735:842b5e7dcac8 52737:7b396ef36af6
   140         case get_option :: export_file :: more_options =>
   140         case get_option :: export_file :: more_options =>
   141           val options = (Options.init() /: more_options)(_ + _)
   141           val options = (Options.init() /: more_options)(_ + _)
   142 
   142 
   143           if (get_option != "")
   143           if (get_option != "")
   144             java.lang.System.out.println(options.check_name(get_option).value)
   144             java.lang.System.out.println(options.check_name(get_option).value)
   145           else if (export_file != "")
   145 
       
   146           if (export_file != "")
   146             File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   147             File.write(Path.explode(export_file), YXML.string_of_body(options.encode))
   147           else java.lang.System.out.println(options.print)
   148 
       
   149           if (get_option == "" && export_file == "")
       
   150             java.lang.System.out.println(options.print)
   148 
   151 
   149           0
   152           0
   150         case _ => error("Bad arguments:\n" + cat_lines(args))
   153         case _ => error("Bad arguments:\n" + cat_lines(args))
   151       }
   154       }
   152     }
   155     }