On 07/24/2012 02:07 AM, Stefan Monnier wrote:
> Could you separate this part of the patch, since I don't know what you
> mean by "inlining by hand".

Sure, attached; this assumes the earlier patch in
<http://debbugs.gnu.org/cgi/bugreport.cgi?bug=11935#5>
has been applied and merged.