Move RSS feed for commits to this channel?

Stream: batteries

[Joscha Mennicken]

Hi, is there any interest in moving the rss feed of commits from #rss > Recent Commits to batteries:main to this channel? E.g. #CSLib > Recent commits to cslib or #PhysLean > Recent commits to PhysLean. (See also #CSLib > RSS feed for CSLib commits @ 💬.) Not sure if it would be an improvement or not.

[Michael Rothgang]

As a mathlib contributor, I quite like learning about changes to batteries in #rss, without having to subscribe to the batteries stream. As mathlib depends on batteries, including it seems very useful. Moving this to this channel would a net negative for me personally.

[Michael Rothgang]

Of course, I don't mind you duplicating the notifications here. (Perhaps that would be useful. It might fragment any discussion on that stream, but arguably that's the wrong place for longer discussions anyway.)

[Kevin Buzzard]

My impression is that the general rule is that we have "mostly posted to by bots" channels and "mostly posted to by humans" channels, and this suggestion would violate that, however as you point out, other projects seem to be doing it.

[Kim Morrison]

Yes, my personal preference is to keep them (all) in #rss.

[Chris Henson]

Moving the CSLib one to #rss is fine by me.

[Joscha Mennicken]

I can make the bot post in #rss if someone with enough permissions moves the feeds.

[Johan Commelin]

@Joscha Mennicken Just to confirm: you mean this thread? #CSLib > Recent commits to cslib

[Joscha Mennicken]

@Johan Commelin The only two github streams currently not in #rss are #CSLib > Recent commits to cslib and #PhysLean > Recent commits to PhysLean.

I've halted all the rss feeds (including in #rss), so you can also rename the ones in #rss for consistency by dropping the :main or :master at the end, if you want (or by adding the suffix to the newly moved streams, of course). I'll match the names when I start the feeds back up.

[Johan Commelin]

Sorry for the delay. Move executed.