notification groups: add information about how to ping them#1818

spastorino merged 1 commit intorust-lang:masterrust-lang/rustc-dev-guide:masterfrom

RalfJung:notification-groupsRalfJung/rustc-dev-guide:notification-groupsCopy head branch name to clipboard