# HG changeset patch
# User wenzelm
# Date 1645458621 -3600
# Node ID 4b3ae1a3bbbded6fb02da5e56d7a9480e942e394
# Parent  001b74439ad4c4250fcbed63e4378ee86242cf38
more robust;

diff -r 001b74439ad4 -r 4b3ae1a3bbbd src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Mon Feb 21 16:48:44 2022 +0100
+++ b/src/Pure/General/http.scala	Mon Feb 21 16:50:21 2022 +0100
@@ -344,8 +344,8 @@
     def apply(request: Request): Option[Response] =
       for {
         p <- request.uri_path
-        path = Path.explode("$ISABELLE_PDFJS_HOME") + p
-        if path.is_file
+        path = Path.explode("$ISABELLE_PDFJS_HOME") + p if path.is_file
+        s = p.implode if s.startsWith("build/") || s.startsWith("web/")
       } yield Response.read(path)
   }
 }
\ No newline at end of file