equal
deleted
inserted
replaced
360 NONE => [] |
360 NONE => [] |
361 | SOME path => map (document_job path false) documents); |
361 | SOME path => map (document_job path false) documents); |
362 |
362 |
363 val _ = |
363 val _ = |
364 if not (null jobs) andalso null doc_files then |
364 if not (null jobs) andalso null doc_files then |
365 Output.physical_stderr ("### Document preparation for session " ^ quote name ^ |
365 Output.physical_stderr ("### Legacy feature! Document preparation for session " ^ quote name ^ |
366 " without 'document_files'\n") |
366 " without 'document_files'\n") |
367 else (); |
367 else (); |
368 |
368 |
369 val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>); |
369 val _ = jobs |> Par_List.map (fn job => job ()) |> List.app (op |>); |
370 in |
370 in |