leanprover-community / mathlib

  • Home
  • Zulip archive
  • API documentation
  • Lean web editor
  • Links

Zulip Chat Archive

Stream: batteries

Topic: Mergeable lean testing PRs bot


Kim Morrison (May 24 2025 at 08:58):

Would anyone be willing to port the "Mergeable lean testing PRs" bot from Mathlib to Batteries? It would regularly, e.g. this evening, be useful in keeping Batteries up to date with nightly releases.

Kim Morrison (May 24 2025 at 09:32):

ah, I did it: https://github.com/leanprover-community/batteries/pull/1239


Last updated: Dec 20 2025 at 21:32 UTC

Theme Simple by wildflame © 2016 Powered by jekyll