Skip to content

Commit 01954c4

Browse files
fix: tutorial header permalinks (#861)
Bumps dependencies to fix two bugs in tutorial header permalink widgets: 1. They were absolute, rather than relative, URLs, so they ignored `<base>` 2. They had doubled components in their HTML IDs
1 parent 016b4d6 commit 01954c4

2 files changed

Lines changed: 14 additions & 7 deletions

File tree

TutorialMain.lean

Lines changed: 12 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -19,11 +19,18 @@ def plausible := {{
1919
<script defer="defer" data-domain="lean-lang.org" src="https://plausible.io/js/script.outbound-links.js"></script>
2020
}}
2121

22-
23-
def version (_content : Array (Verso.Doc.Inline g)) : Verso.Doc.Inline g := .text Lean.versionString
24-
25-
def manualLink (args : Array (Verso.Doc.Inline g)) : Verso.Doc.Inline g:=
26-
Verso.Doc.Inline.link args Lean.manualRoot
22+
section
23+
open Verso.Doc.Elab
24+
open Lean
25+
@[role]
26+
def version : RoleExpanderOf Unit
27+
| (), _ => ``(Verso.Doc.Inline.text $(quote Lean.versionString))
28+
29+
@[role]
30+
def manualLink : RoleExpanderOf Unit
31+
| (), content => do
32+
``(Verso.Doc.Inline.link #[$[$(← content.mapM elabInline)],*] Lean.manualRoot)
33+
end
2734

2835
open Verso.Doc Concrete in
2936
def tutorials : Tutorials where

lake-manifest.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
"type": "git",
66
"subDir": null,
77
"scope": "",
8-
"rev": "916bb962ceb8b88e6a731db6d28e862f99e834c4",
8+
"rev": "4c6b02ee232211811f9ad1c148ac336122e256d7",
99
"name": "verso",
1010
"manifestFile": "lake-manifest.json",
1111
"inputRev": "main",
@@ -25,7 +25,7 @@
2525
"type": "git",
2626
"subDir": null,
2727
"scope": "",
28-
"rev": "8bdc0cf15a6bbb6906e0d7925907e2c913c7c29b",
28+
"rev": "a252e45ae646f999c535e1056536def2c871f085",
2929
"name": "versowebcomponents",
3030
"manifestFile": "lake-manifest.json",
3131
"inputRev": "main",

0 commit comments

Comments
 (0)