<br><br>On Wednesday, 8 August 2012, Michael Stahl  wrote:<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
binfilter was completely broken; if you remove stuff from tools please<br>
build with --enable-binfilter.  i just spent the last 2 hours fixing<br>

<br>
</blockquote><div><br></div><div>Oh dear. Very sorry. Will take that into consideration in future.  <span></span></div>