@nikomatsakis what would it take to get an email alias somewhere that we could set up to receive CI notifications for miri?
Currently whoever pushed the last thing to master gets the cron job failure notifications, which is far from ideal
(it'd take me no time to set up
firstname.lastname@example.org, but maybe that wouldn't be the best place for this alias)
I .. don't know
maybe ask somebody in the infra team (on Discord, I think)
@RalfJ alex mentioned that in our meeting today. Lists are done thru DNS and it's kind of annoying to edit frequently, but they can exist.
lists through... DNS? I don't think I understand, but whatever.^^
@Oli what do you think?
through our dns provider
Whatever works, works for me.