Should I update my PR?  It's too bad that github doesn't handle this more cleanly.  (This is trivial and I don't personally care who fixes it.)