<div dir="ltr"><div class="gmail_extra">Thanks everyone. I didn't expect just continuing "make" would work, but it does, so that's a workaround for now. I'll look forward to the real fix, of course.</div><div class="gmail_extra"><br></div><div class="gmail_extra">John</div></div>