src/Pure/Tools/dump.scala
changeset 68744 64fb127e33f7
parent 68743 91162dd89571
parent 68741 e90cf766723c
child 68758 a110e7e24e55
equal deleted inserted replaced
68743:91162dd89571 68744:64fb127e33f7
   192       "O:" -> (arg => output_dir = Path.explode(arg)),
   192       "O:" -> (arg => output_dir = Path.explode(arg)),
   193       "R" -> (_ => requirements = true),
   193       "R" -> (_ => requirements = true),
   194       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   194       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
   195       "a" -> (_ => all_sessions = true),
   195       "a" -> (_ => all_sessions = true),
   196       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
   196       "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
       
   197       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
   197       "l:" -> (arg => logic = arg),
   198       "l:" -> (arg => logic = arg),
   198       "g:" -> (arg => session_groups = session_groups ::: List(arg)),
       
   199       "o:" -> (arg => options = options + arg),
   199       "o:" -> (arg => options = options + arg),
   200       "s" -> (_ => system_mode = true),
   200       "s" -> (_ => system_mode = true),
   201       "v" -> (_ => verbose = true),
   201       "v" -> (_ => verbose = true),
   202       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   202       "x:" -> (arg => exclude_sessions = exclude_sessions ::: List(arg)))
   203 
   203