equal
deleted
inserted
replaced
378 val store = Sessions.store(system_mode) |
378 val store = Sessions.store(system_mode) |
379 |
379 |
380 |
380 |
381 /* session selection and dependencies */ |
381 /* session selection and dependencies */ |
382 |
382 |
383 val full_sessions = Sessions.load(build_options, dirs, select_dirs) |
383 val full_sessions = |
|
384 Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs) |
384 |
385 |
385 def sources_stamp(deps: Sessions.Deps, name: String): String = |
386 def sources_stamp(deps: Sessions.Deps, name: String): String = |
386 { |
387 { |
387 val digests = |
388 val digests = |
388 full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name) |
389 full_sessions(name).meta_digest :: deps.sources(name) ::: deps.imported_sources(name) |