src/Pure/Admin/build_doc.scala
changeset 67023 e27e05d6f2a7
parent 65519 d244d8f8e13f
child 67026 687c822ee5e3
     1.1 --- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 11:11:37 2017 +0100
     1.2 +++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 15:45:33 2017 +0100
     1.3 @@ -22,13 +22,15 @@
     1.4      system_mode: Boolean = false,
     1.5      docs: List[String] = Nil): Int =
     1.6    {
     1.7 +    val sessions_structure = Sessions.load(options)
     1.8      val selection =
     1.9        for {
    1.10 -        info <- Sessions.load(options).build_topological_order
    1.11 +        name <- sessions_structure.build_topological_order
    1.12 +        info = sessions_structure(name)
    1.13          if info.groups.contains("doc")
    1.14          doc = info.options.string("document_variants")
    1.15          if all_docs || docs.contains(doc)
    1.16 -      } yield (doc, info.name)
    1.17 +      } yield (doc, name)
    1.18  
    1.19      val selected_docs = selection.map(_._1)
    1.20      val sessions = selection.map(_._2)