Skip to content

Commit

Permalink
fix: fields of ThousandPlusTheorem (#560)
Browse files Browse the repository at this point in the history
Proper fix for #559: depends on leanprover-community/mathlib4#20066
  • Loading branch information
grunweg authored Dec 19, 2024
1 parent 793ba9d commit 3c0ed34
Showing 1 changed file with 3 additions and 4 deletions.
7 changes: 3 additions & 4 deletions make_site.py
Original file line number Diff line number Diff line change
Expand Up @@ -185,12 +185,11 @@ class ThousandPlusTheorem:
decls: Optional[List[str]] = None
doc_decls: Optional[List[DocDecl]] = None
author: Optional[str] = None
links: Optional[Mapping[str, str]] = None
date: Optional[str] = None
url: Optional[str] = None
note: Optional[str] = None
# TODO: workaround for build failure caused by tags in Q208416
url: Optional[str] = None
identifiers: Optional[str] = None
date: Optional[str] = None


@dataclass
class Event:
Expand Down

0 comments on commit 3c0ed34

Please sign in to comment.