tuned;
authorwenzelm
Sat Aug 11 17:28:20 2018 +0200 (4 months ago)
changeset 68741e90cf766723c
parent 68740 682ff0e84387
child 68742 a6cc4302c380
tuned;
src/Pure/Tools/dump.scala
     1.1 --- a/src/Pure/Tools/dump.scala	Sat Aug 11 16:02:55 2018 +0200
     1.2 +++ b/src/Pure/Tools/dump.scala	Sat Aug 11 17:28:20 2018 +0200
     1.3 @@ -194,8 +194,8 @@
     1.4        "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
     1.5        "a" -> (_ => all_sessions = true),
     1.6        "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
     1.7 +      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
     1.8        "l:" -> (arg => logic = arg),
     1.9 -      "g:" -> (arg => session_groups = session_groups ::: List(arg)),
    1.10        "o:" -> (arg => options = options + arg),
    1.11        "s" -> (_ => system_mode = true),
    1.12        "v" -> (_ => verbose = true),