Closed eric-wieser closed 11 months ago
bors merge
Pull request successfully merged into master.
Build succeeded!
The publicly hosted instance of bors-ng is deprecated and will go away soon.
If you want to self-host your own instance, instructions are here. For more help, visit the forum.
If you want to switch to GitHub's built-in merge queue, visit their help page.
Also correct links to point to the lean3 webpages; this means that users clicking them end up on pages which also have scary banners telling them not to use Lean 3.