# HG changeset patch # User wenzelm # Date 1510087253 -3600 # Node ID a9859e879f38353a2fee0f8eb596ff51fc54b388 # Parent d6d9fd2559ce460ed5cdd527b821ec60e96a9a0c proper build_selection for clean_build (amending 961285f581e6): e.g. relevant for "isabelle build_doc"; diff -r d6d9fd2559ce -r a9859e879f38 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Nov 07 21:32:22 2017 +0100 +++ b/src/Pure/Tools/build.scala Tue Nov 07 21:40:53 2017 +0100 @@ -391,13 +391,13 @@ SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString } + val selection1 = + Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, + exclude_sessions, session_groups, sessions) ++ selection + val (selected_sessions, deps) = { - val selected_sessions0 = - full_sessions.selection( - Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups, - exclude_sessions, session_groups, sessions) ++ selection) - + val selected_sessions0 = full_sessions.selection(selection1) val deps0 = Sessions.deps(selected_sessions0, full_sessions.global_theories, progress = progress, inlined_files = true, verbose = verbose, @@ -450,7 +450,7 @@ // optional cleanup if (clean_build) { - for (name <- full_sessions.build_descendants(selected_sessions.build_topological_order)) { + for (name <- full_sessions.build_descendants(full_sessions.build_selection(selection1))) { val files = List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)). map(store.output_dir + _).filter(_.is_file)