Zulip Chat Archive
Stream: batteries
Topic: lean 6397
Johan Commelin (Dec 18 2024 at 05:36):
This PR fixes the build on the branch lean-pr-testing-6397.
https://github.com/leanprover-community/batteries/pull/1076
François G. Dorais (Dec 18 2024 at 05:57):
@Kim Morrison Why can't Johan just push into that branch?
Johan Commelin (Dec 18 2024 at 05:58):
Ooh, turns out I can!
Johan Commelin (Dec 18 2024 at 05:59):
Some time in the past I couldn't. Didn't know that my powers had changed
François G. Dorais (Dec 18 2024 at 05:59):
Excellent! Mind the long lines though :smile:
François G. Dorais (Dec 18 2024 at 06:02):
Sorry @Kim Morrison! Situation resolved.
Last updated: May 02 2025 at 03:31 UTC