Commit 2024-03-24 01:16 5fc4f861

ci: Import Archive when checking YAML files (#11562) We sometimes want to refer to Archive declarations in the YAML files. This is currently impossible because the script in checkYaml only imports Mathlib. This PR changes it to also import Archive. It also changes the hyperlinks to Archive to instead list declarations directly. Also fix the fallout from #11530 that CI didn't catch that because we forgot to pipe the errors coming from lake build Archive (see #11612).