Re: How to manage github pull requests?

Hi Martin,

After migration to git in the Russian repo,
I updated the ids to the last English git id (even if the git diff was empty).

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.

If you already have an established workflow, based on exactly the last git id,
I think you can make a change (or ask George) in EnCommitHashesParser to not ignore these commits.

[1] https://gitlab.com/php-infrastructe/doc/-/blob/master/src/Helper/EnCommitHashesParser.php#L11

wbr,
Sergey Panteleev
On 3 Feb 2021, 14:16 +0300, Martin Samesch <[email protected]>, wrote:
>
> But there's no problem with bumping EN-Rev to the latest revision
> either, even when the diff is empty? I'm asking, because I don't care
> about editing EN-Rev and have a script doing it after sync/review. And
> my updated svn revcheck only compares EN-Rev against the latest
> revision.