batteries PR adaptations

Stream: batteries

[Yury G. Kudryashov]

Hi, I've just opened batteries#1052. Am I supposed to push Mathlib fixes to branch#batteries-pr-testing-1052 or create a new branch on top of it, because this one will be overriden by the Batteries CI?

[Kim Morrison]

No, you can push directly to batteries-pr-testing-1052.

[Kim Morrison]

I don't think any of the automation will overwrite what you do: there's automation to create the branch, but it doesn't do anything subsequently except report build results back to the batteries PR.

[Yury G. Kudryashov]

Thanks! I'll open a PR to add this information to README and the autogenerated comment.