src/Pure/Tools/server_commands.scala
changeset 71981 0be06f99b210
parent 71896 ce06d6456cc8
child 72163 f5722290a4d0
equal deleted inserted replaced
71980:6441b4591eb8 71981:0be06f99b210
    55         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
    55         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
    56           include_sessions = args.include_sessions)
    56           include_sessions = args.include_sessions)
    57       val base = base_info.check_base
    57       val base = base_info.check_base
    58 
    58 
    59       val results =
    59       val results =
    60         Build.build(options, Sessions.Selection.session(args.session),
    60         Build.build(options,
       
    61           selection = Sessions.Selection.session(args.session),
    61           progress = progress,
    62           progress = progress,
    62           build_heap = true,
    63           build_heap = true,
    63           dirs = dirs,
    64           dirs = dirs,
    64           infos = base_info.infos,
    65           infos = base_info.infos,
    65           verbose = args.verbose)
    66           verbose = args.verbose)