equal
deleted
inserted
replaced
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 } |