<div dir="ltr"><br><br><div class="gmail_quote"><div dir="ltr">On Thu, Jan 14, 2016 at 2:24 PM Tobias Grosser <<a href="mailto:tobias@grosser.es">tobias@grosser.es</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On 01/14/2016 07:02 PM, Eric Christopher wrote:<br>
> And, to be honest, if they're still failing after a bit we should<br>
> probably just remove them as they're unmaintained :)<br>
><br>
> That said, Dave and I were talking yesterday about needing to fix the<br>
> gdb bot :)<br>
<br>
Just wanted to give a headsup. Some people may just have missed to<br>
update their bots. Also, it would probably be nice to disable the<br>
remaining bots maybe a day before the commit, such that we do not<br>
suddenly have a buildbot console full of red bots.<br>
<br></blockquote><div><br></div><div>Sure. Galina? :)</div><div><br></div><div>-eric</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Best,<br>
Tobias<br>
</blockquote></div></div>