fix: remove obsolete syntax workaround and fix proof states

leanprover · Dec 18, 2024 · de82a3b · de82a3b
1 parent b4623a7
commit de82a3b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/verso/Verso/Code/Highlighted.lean b/src/verso/Verso/Code/Highlighted.lean
@@ -366,7 +366,7 @@ partial defmethod Highlighted.toHtml : Highlighted → HighlightHtmlM Html
       let id := s!"tactic-state-{hash info}-{startPos}-{endPos}"
       pure {{
         <span class="tactic">
-          <label «for»={{id}}>{{← toHtml hl}}</label>
+          <label for={{id}}>{{← toHtml hl}}</label>
           <input type="checkbox" class="tactic-toggle" id={{id}}></input>
           <span class="tactic-state">
             {{← if info.isEmpty then