# HG changeset patch # User wenzelm # Date 1636634852 -3600 # Node ID eaeab1358ced2d163e77fe56fc6ba783e77117d3 # Parent ab48dfc2b25118f330e5fd667a59c7c1935e4409 more robust; diff -r ab48dfc2b251 -r eaeab1358ced src/Pure/Thy/html.scala --- a/src/Pure/Thy/html.scala Thu Nov 11 13:18:35 2021 +0100 +++ b/src/Pure/Thy/html.scala Thu Nov 11 13:47:32 2021 +0100 @@ -420,7 +420,8 @@ base match { case None => "" case Some(base_dir) => - File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile).implode + val path = File.path(dir.absolute.java_path.relativize(base_dir.absolute.java_path).toFile) + if (path.is_current) "" else path.implode + "/" } def isabelle_css: Path = Path.explode("~~/etc/isabelle.css")