<div dir="ltr"><div class="gmail_extra"><br><div class="gmail_quote">On Mon, May 12, 2014 at 4:58 PM, Richard Eisenberg <span dir="ltr"><<a href="mailto:eir@cis.upenn.edu" target="_blank">eir@cis.upenn.edu</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">We could, of course, just leave the functions there with new implementations, but that feels like it could accumulate legacy functions over time.</blockquote>
</div><br>I think the ultimate goal of removing the function was not unwise of you, but the right thing to do here would be to write a reimplementation, mark it as {-# DEPRECATED #-}, and give a timetable for its future removal. This gives users time to adjust and minimizes breakage.<br>
<br clear="all"><div>G</div>-- <br>Gregory Collins <<a href="mailto:greg@gregorycollins.net" target="_blank">greg@gregorycollins.net</a>>
</div></div>