src/Pure/General/http.scala
changeset 75117 4b3ae1a3bbbd
parent 75113 a7a489ea4661
child 75119 7bf685cbc789
--- 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