Yes, last night's build worked for me, thanks.<br><br><div><span class="gmail_quote">On 11/21/05, <b class="gmail_sendername">Simon Peyton-Jones</b> &lt;<a href="mailto:simonpj@microsoft.com">simonpj@microsoft.com</a>&gt; wrote:
</span><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">I believe I have fixed this.&nbsp;&nbsp;(It was my fault, late last week.)<br><br>I'm compiling now to test.&nbsp;&nbsp;Meanwhile it'd be worth your having another
<br>go.<br><br>Simon<br><br></blockquote></div><br>