<div class="gmail_quote">On Fri, Aug 12, 2011 at 11:06, Matthew Flatt <span dir="ltr">&lt;<a href="mailto:mflatt@cs.utah.edu">mflatt@cs.utah.edu</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin: 0pt 0pt 0pt 0.8ex; border-left: 1px solid rgb(204, 204, 204); padding-left: 1ex;">

We&#39;ve made some repairs in that area since 5.1.2, but I don&#39;t know if<br>
we&#39;ve solved the problem that you&#39;re seeing. Which version of gcc are<br>
you using?<br>
<div><div></div><br></div></blockquote><div><br>$ gcc --version<br>gcc (GCC) 4.1.2 20080704 (Red Hat 4.1.2-50)<br> </div></div>