# HG changeset patch
# User wenzelm
# Date 1660914364 -7200
# Node ID dce94a1d18fd88e1bd57d6291d4d987ee5c97c4a
# Parent  0f46e06030e98a686c53a1d158a1a431c49758bf
proper permissive = true (amending 475fedc02737)

diff -r 0f46e06030e9 -r dce94a1d18fd 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)