--- a/src/Pure/Admin/build_doc.scala Tue Nov 07 11:11:37 2017 +0100
+++ b/src/Pure/Admin/build_doc.scala Tue Nov 07 15:45:33 2017 +0100
@@ -22,13 +22,15 @@
system_mode: Boolean = false,
docs: List[String] = Nil): Int =
{
+ val sessions_structure = Sessions.load(options)
val selection =
for {
- info <- Sessions.load(options).build_topological_order
+ name <- sessions_structure.build_topological_order
+ info = sessions_structure(name)
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
- } yield (doc, info.name)
+ } yield (doc, name)
val selected_docs = selection.map(_._1)
val sessions = selection.map(_._2)