<div><br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="auto">On Th, 3 May 2018 at 13:53 UTC, Joachim Breitner wrote:</div><div dir="auto"><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">I am worried about the </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">signal-to-noise ratio for those poor committee members¬†</span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">who have not </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">given up on following the GitHub notifications for the ghc-proposals </span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">repository.</span><span style="white-space:pre-wrap;background-color:rgb(255,255,255)">...</span></div><div dir="auto"><span style="white-space:pre-wrap;background-color:rgb(255,255,255)"><br></span></div><div dir="auto"></div></blockquote><div dir="auto"><br></div><div dir="auto">Almost by definition, Issue-tracker traffic should <i>not</i>¬†be going to committee members, unless they deliberately opt in to some issue.</div><div dir="auto"><br></div><div dir="auto">I don't get github traffic except for proposals I've opted in to; and I can always 'mute the thread'. So specifically no traffic for the Issue David's just raised [good]. I go and sweep github for interesting pickings every now and then, and subscribe.</div><div dir="auto"><br></div><div dir="auto">Looks like (from his puzzled reply) Simon did get traffic for that issue. I dread to think what other github traffic Simon might have suffered recently.</div><div dir="auto"><br></div><div dir="auto">Can a user configure to get proposal traffic but not Issue tracker traffic? (There seem to be options for everything.) I suggest the committee members do that.</div><div dir="auto"><br></div><div dir="auto">AntC</div></div></div>