more robust;
authorwenzelm
Mon, 21 Feb 2022 16:50:21 +0100
changeset 75117 4b3ae1a3bbbd
parent 75116 001b74439ad4
child 75118 6fd8e482c9ce
more robust;
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