diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 775524b..cc39fac 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -14,8 +14,13 @@ open Lean open scoped DocGen4.Jsx def moduleListFile (file : NameExt) : BaseHtmlM Html := do + let contents := + if file.ext == .pdf then + {s!"🗎 {file.getString!} (pdf)"} + else + {file.getString!} return
- {file.getString!} + {contents}
/-- diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean index 2966f40..d1be339 100644 --- a/DocGen4/Process/NameExt.lean +++ b/DocGen4/Process/NameExt.lean @@ -42,8 +42,7 @@ def cmp (n₁ n₂ : NameExt) : Ordering := | ord => ord def getString! : NameExt → String - | ⟨str _ s, .html⟩ => s - | ⟨str _ s, .pdf⟩ => s ++ ".pdf" + | ⟨str _ s, _⟩ => s | _ => unreachable! end NameExt diff --git a/static/style.css b/static/style.css index ae00a45..f8b37b6 100644 --- a/static/style.css +++ b/static/style.css @@ -751,7 +751,6 @@ a:link, a:visited, a:active { a.pdf:link, a.pdf:visited, a.pdf:active { color:var(--link-pdf-color); - text-decoration: none } /** Show it on hover though. **/