On Mon, Apr 2, 2012 at 21:07, Matthew Flatt <span dir="ltr">&lt;<a href="mailto:mflatt@cs.utah.edu">mflatt@cs.utah.edu</a>&gt;</span> wrote:<br><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">

I&#39;ve changed the limit to 1024, which brings it back in sync with<br>
`font%&#39;.<br>
[...] I&#39;ll continue investigating.</blockquote><div><br><br>Thank you Matthew.<br><br><br></div></div><br>