src/Pure/Build/browser_info.scala
changeset 82147 3f7c8e6d3481
parent 82142 508a673c87ac
child 82152 3312ca0f3915
--- a/src/Pure/Build/browser_info.scala	Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/browser_info.scala	Wed Feb 12 14:28:32 2025 +0100
@@ -638,7 +638,7 @@
           val html = context.source(node_context(file, file_dir).make_html(thy_elements, xml))
 
           val path = Path.explode(file)
-          val src_path = File.relative_path(master_dir, path).getOrElse(path)
+          val src_path = File.perhaps_relative_path(master_dir, path)
 
           val file_title = "File " + Symbol.cartouche_decoded(src_path.implode_short)
           HTML.write_document(file_dir, file_html.file_name,