equal
deleted
inserted
replaced
53 case (doc, session) => |
53 case (doc, session) => |
54 try { |
54 try { |
55 progress.echo("Documentation " + quote(doc) + " ...") |
55 progress.echo("Documentation " + quote(doc) + " ...") |
56 |
56 |
57 using(store.open_database_context())(db_context => |
57 using(store.open_database_context())(db_context => |
58 Presentation.build_documents(session, deps, db_context, |
58 Document_Build.build_documents(session, deps, db_context, |
59 output_pdf = Some(Path.explode("~~/doc")))) |
59 output_pdf = Some(Path.explode("~~/doc")))) |
60 None |
60 None |
61 } |
61 } |
62 catch { |
62 catch { |
63 case Exn.Interrupt.ERROR(msg) => |
63 case Exn.Interrupt.ERROR(msg) => |