commit messages

Stream: mathlib4

[Bulhwi Cha]

rss-bot said:

chore: silence deprecation warning in DirectSumIsInternal (mathlib4#6416)

@eric-wieser, would you be able to find a better solution to this?

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Authored-by: semorrison (commit)

rss-bot said:

chore: bump leantar version (mathlib4#6430)

This fixes the issue that leantar-0.1.4.exe was not actually statically linked on windows, reported by @MohanadAhmed . Could someone using MacOS aarch64 check that this still works? All other OSs should be unaffected.

Authored-by: digama0 (commit)

I think we should separate discussions from commit messages.

[Scott Morrison]

The trick here is to remember to leave comments you don't want to preserve underneath the --- in the PR description. (Reminding myself. :-)