--- 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,
--- a/src/Pure/Build/build.scala Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/build.scala Wed Feb 12 14:28:32 2025 +0100
@@ -728,7 +728,7 @@
val blobs =
blobs_files.map { name =>
val path = Path.explode(name)
- val src_path = File.relative_path(master_dir, path).getOrElse(path)
+ val src_path = File.perhaps_relative_path(master_dir, path)
val file = read_source_file(name)
val bytes = file.bytes
--- a/src/Pure/Build/sessions.scala Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/Build/sessions.scala Wed Feb 12 14:28:32 2025 +0100
@@ -418,7 +418,7 @@
name <- proper_session_theories.iterator
path = Path.explode(name.master_dir)
if !ok(path.canonical_file)
- path1 = File.relative_path(info.dir.canonical, path).getOrElse(path)
+ path1 = File.perhaps_relative_path(info.dir.canonical, path)
} yield (path1, name)).toList
val bad_dirs = (for { (path1, _) <- bad } yield path1.toString).distinct.sorted
--- a/src/Pure/General/file.scala Wed Feb 12 14:26:43 2025 +0100
+++ b/src/Pure/General/file.scala Wed Feb 12 14:28:32 2025 +0100
@@ -123,6 +123,9 @@
else None
}
+ def perhaps_relative_path(base: Path, other: Path): Path =
+ relative_path(base, other).getOrElse(other)
+
/* bash path */