Policy on removal of push?

Is there a procedure to take regarding removal of a push to the github repo or do you simply close it. I would like to re-submit a push request against the 5.5 branch while removing the old push request. Also can I obtain some information on the current state of new function extending regarding acceptance of a patch for bug #38917? (bug report/feature request at https://bugs.php.net/bug.php?id=38917) And last but not least does an RFC need to be created for this type of extended functionality or would function documentation suffice? Thanks, -- Jas <http://phpdhcpadmin.sourceforge.net>