Re: How to manage github pull requests?
| From: | Martin Samesch | Date: | Wed, 03 Feb 2021 13:29:17 +0000 |
| Subject: | Re: How to manage github pull requests? | ||
| References: | 1 2 3 4 5 6 7 8 9 10 | Groups: | php.doc |
| Request: | Send a blank email to phpdoc+get-969387839@lists.php.net to get a copy of this message | ||
Hi Sergey,
On Wed, Feb 03, 2021 at 03:00:46PM +0300, Sergey Panteleev wrote:
> [...]
> Yesterday I updated the logic:
> Currently, I'm getting the latest git id, except three ids [1].
> If the latest English git id is one of them, I get the previous one.
thanks for your explanation. Now I got it. I'll also adapt my srcipt to
ignore these ids, then.
Cheers,
Martin