changeset 71632 | c1bc38327bc2 |
parent 71601 | 97ccf48c2f0c |
child 71684 | 5036edb025b7 |
71631:3f02bc5a5a03 | 71632:c1bc38327bc2 |
---|---|
577 |
577 |
578 /** command line entry point **/ |
578 /** command line entry point **/ |
579 |
579 |
580 def main(args: Array[String]) |
580 def main(args: Array[String]) |
581 { |
581 { |
582 Command_Line.tool0 { |
582 Command_Line.tool { |
583 var force = false |
583 var force = false |
584 var verbose = false |
584 var verbose = false |
585 var exclude_task = Set.empty[String] |
585 var exclude_task = Set.empty[String] |
586 |
586 |
587 val getopts = Getopts(""" |
587 val getopts = Getopts(""" |