On 2/19/07, <b class="gmail_sendername">Malcolm Wallace</b> &lt;<a href="mailto:Malcolm.Wallace@cs.york.ac.uk">Malcolm.Wallace@cs.york.ac.uk</a>&gt; wrote:<div><span class="gmail_quote"></span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
&gt; Whoops, silly error on my part. I&#39;ve pushed another patch. Please try<br>&gt; the new one.<br></blockquote></div><br>Sorry, it&#39;s there now.<br><br>Andrew<br><br>