proper permissive = true (amending 475fedc02737)
authorwenzelm
Fri, 19 Aug 2022 15:06:04 +0200
changeset 75903 dce94a1d18fd
parent 75902 0f46e06030e9
child 75904 6d9d9a395533
proper permissive = true (amending 475fedc02737)
src/Pure/Tools/build_job.scala
--- 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)