From 252003f58ac50916c56005555604e9785530d2d0 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 16 Dec 2024 20:14:49 +0100
Subject: [PATCH] fix: logo link relativized incorrectly when --site-base
 provided

---
 src/verso-manual/VersoManual.lean       | 8 +++++++-
 src/verso-manual/VersoManual/Basic.lean | 4 ++++
 src/verso-manual/VersoManual/Html.lean  | 2 +-
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 85aa4f9..a9d5489 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -123,6 +123,8 @@ structure Config where
   draft : Bool := false
   /-- The URL from which to draw the logo to show, if any -/
   logo : Option String := none
+  /-- The URL that the logo should link to, if any (default is site root) -/
+  logoLink : Option String := none
   /-- URL for source link -/
   sourceLink : Option String := none
   /-- URL for issue reports -/
@@ -276,6 +278,7 @@ def page (toc : List Html.Toc) (path : Path) (textTitle : String) (htmlTitle con
     (showNavButtons := showNavButtons)
     (base := config.baseURL)
     (logo := config.logo)
+    (logoLink := config.logoLink)
     (repoLink := config.sourceLink)
     (issueLink := config.issueLink)
     (extraStylesheets := config.extraCss ++ state.extraCssFiles.toList.map ("/-verso-css/" ++ ·.1))
@@ -479,12 +482,15 @@ where
     | ("--without-html-multi"::more) => opts {cfg with emitHtmlMulti := false} more
     | ("--with-word-count"::file::more) => opts {cfg with wordCount := some file} more
     | ("--without-word-count"::more) => opts {cfg with wordCount := none} more
-    | ("--site-base-url"::base::more) => opts {cfg with baseURL := some base} more
+    | ("--site-base-url"::base::more) => opts {cfg with baseURL := some (fixBase base)} more
     | ("--draft"::more) => opts {cfg with draft := true} more
     | ("--verbose"::more) => opts {cfg with verbose := true} more
     | (other :: _) => throw (↑ s!"Unknown option {other}")
     | [] => pure cfg
 
+  fixBase (base : String) : String :=
+    if base.takeRight 1 != "/" then base ++ "/" else base
+
   go : ReaderT ExtensionImpls IO UInt32 := do
     let hasError ← IO.mkRef false
     let logError msg := do hasError.set true; IO.eprintln msg
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 33d43fc..ea69d78 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -129,6 +129,10 @@ def relativize (path : Path) (url : String) : String := Id.run do
 #guard_msgs in
 #eval Path.relativize #["a", "b", "c", "d", "e"] "/a/b/c"
 
+/-- info: "" -/
+#guard_msgs in
+#eval Path.relativize #[] "/"
+
 end Path
 
 /--
diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean
index d260998..5b98ab9 100644
--- a/src/verso-manual/VersoManual/Html.lean
+++ b/src/verso-manual/VersoManual/Html.lean
@@ -505,7 +505,7 @@ def page
                   let logoHtml := {{<img src={{url}}/>}}
                   let logoDest :=
                     if let some root := logoLink then root
-                    else relativeRoot
+                    else "/"
                   {{<a href={{logoDest}} id="logo">{{logoHtml}}</a>}}
                 else .empty }}
               {{if showNavButtons then toc.navButtons path else .empty}}