On 2015-03-18 20:37, Walter Bright wrote: > Why use the tool if you're going to ignore it? It's tremendously useful for reporting other issues. I can configure the tool to not report the this issue but sometimes it's just easier to ignore. -- /Jacob Carlborg