src/Pure/Tools/build_job.scala
changeset 72696 7af210f1f13b
parent 72693 0201ae367518
child 72697 e16f85e3c288
equal deleted inserted replaced
72695:45cd55248ffd 72696:7af210f1f13b
   244                   output_pdf = info.document_output,
   244                   output_pdf = info.document_output,
   245                   progress = document_progress,
   245                   progress = document_progress,
   246                   verbose = verbose,
   246                   verbose = verbose,
   247                   verbose_latex = true))
   247                   verbose_latex = true))
   248             using(store.open_database(session_name, output = true))(db =>
   248             using(store.open_database(session_name, output = true))(db =>
   249               for ((doc, pdf) <- documents) {
   249               for (doc <- documents) {
   250                 db.transaction {
   250                 db.transaction {
   251                   Presentation.write_document(db, session_name, doc, pdf)
   251                   Presentation.write_document(db, session_name, doc)
   252                 }
   252                 }
   253               })
   253               })
   254           }
   254           }
   255           Nil
   255           Nil
   256         }
   256         }