changeset 72652 | 07edf1952ab1 |
parent 72599 | 76550282267f |
child 72675 | cc1347c8c804 |
--- a/src/Pure/Admin/build_doc.scala Wed Nov 18 15:47:53 2020 +0100 +++ b/src/Pure/Admin/build_doc.scala Wed Nov 18 15:52:12 2020 +0100 @@ -50,7 +50,7 @@ val errs = Par_List.map((doc_session: (String, String)) => try { - Present.build_documents(doc_session._2, deps, store, progress = progress) + Presentation.build_documents(doc_session._2, deps, store, progress = progress) None } catch {