author | wenzelm |
Fri, 19 Aug 2022 15:06:04 +0200 | |
changeset 75903 | dce94a1d18fd |
parent 75902 | 0f46e06030e9 |
child 75904 | 6d9d9a395533 |
--- a/src/Pure/Tools/build_job.scala Fri Aug 19 14:59:24 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Fri Aug 19 15:06:04 2022 +0200 @@ -26,7 +26,7 @@ for { id <- theory_context.document_id() - (thy_file, blobs_files) <- theory_context.files() + (thy_file, blobs_files) <- theory_context.files(permissive = true) } yield { val node_name = Resources.file_node(Path.explode(thy_file), theory = theory_context.theory)