<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On 5 January 2017 at 02:50, Paul Eggert <span dir="ltr"><<a href="mailto:eggert@cs.ucla.edu" target="_blank">eggert@cs.ucla.edu</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">So how about if we instead use simpler comments that don't contain detail that we'd have to maintain? That should be good enough to document the situation.</blockquote></div><br>Looks good to me. I, and probably our future selves, thank you. ;)<br><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature">--<br>Tim Parenti<br></div></div>
</div></div>