Skip to content

Commit

Permalink
chore(scripts): typo in yaml_check (#4881)
Browse files Browse the repository at this point in the history
  • Loading branch information
hrmacbeth committed Nov 2, 2020
1 parent dae87bc commit 0e4f8f4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion scripts/yaml_check.lean
Expand Up @@ -33,7 +33,7 @@ meta def find_failures (l : list (string × name)) : tactic (list (string × nam
l.mfilter $ λ ⟨key, decl⟩, fails $ get_decl decl

def databases : list (string × string) := [
("undergrad.txt", "Entries in `docs/undergad.yaml` refer to declarations that don't exist. Please correct the following:"),
("undergrad.txt", "Entries in `docs/undergrad.yaml` refer to declarations that don't exist. Please correct the following:"),
("overview.txt", "Entries in `docs/overview.yaml` refer to declarations that don't exist. Please correct the following:"),
("100.txt", "Entries in `docs/100.yaml` refer to declarations that don't exist. Please correct the following:")
]
Expand Down

0 comments on commit 0e4f8f4

Please sign in to comment.