SA5001: clarify message

[arp242]

Clarify the message by putting the function name in there.

Fixes #1489

[dominikh]

@arp242 FYI, I plan to merge all of your PRs once I'm done with some refactoring (which is currently blocked on an x/tools CL). Hopefully soon.

[arp242]

@arp242 FYI, I plan to merge all of your PRs once I'm done with some refactoring (which is currently blocked on an x/tools CL). Hopefully soon.

Coolio, no hurries. I figured something along these lines. Most PRs aren't too large or complex, and don't mind solving any merge conflicts later on (if need be). And if it gets merged next month or whatever then that's fine with me.

I know it's a bit much, but I got some spare time at the moment and I've been planing to fix some of these issues for years, so it's a bit of a "do it now" or "do it never", so "do it now" seems better. But let me know if there's anything you don't want me to do and that's fine.

[ccoVeille]

For this PR and others created by @arp242 I'm confused by the PR status.

It's marked as closed, but the PR wasn't merged. So it's like the code was simply ignored is there something I'm missing?

I feel like the PR number was used in another PR to say "close other PR" while we usually close only issues.

[ccoVeille]

Where there merged by pushing commits to master outside PR consideration?

As I said I might be missing something, but it looks like to me the workflow look like this:

• people opens PRs in branches
• owner cherry pick the commits from these branches
• owner pushes them to master without respecting PR logic or workflow
• PRs are closed as if they were discarded, so not merged

I'm a bit doubtful and lost by this uncommon workflow

And somewhere in the middle, the commit messages are rewritten to mention the initial PRs. Which means to me that if the commits where signed by the one who wrote the commits, so the commit messages where altered from what the user wrote, I'm unsure how it respect the concept of signed commit

[ccoVeille]

I mean it appears to everyone they have been discarded while they were merged

[dominikh]

The PRs were applied by downloading them as patches, applying them, and making minor modifications to the commits as needed. I use https://github.com/leahneukirchen/git-merge-pr for this process. The created commits contain Closes: commands to close the respective PRs. That GitHub cannot differentiate between closing a PR because it was applied in a different way than pushing commits that match the SHAs from the PR and closing a PR because it has been rejected is a fault of GitHub.

[dominikh]

This PR was applied as, and closed by, d39a04f.

[ccoVeille]

This PR was applied as, and closed by, d39a04f.

Yes, it's a commit pushed to master without a PR (apparently), while the current PR was there and ready to be merged

[Xe]

GitHub doesn't have a way to say "this exact patch wasn't merged, but the maintainer downloaded it and merged it themselves after editing it locally", which is halfway between "merged" and "closed". Pull requests only operate on that exact patch being merged, not a similar patch derived from a PR.

[ccoVeille]

Thanks for your replies

I missed this one, I'm only seeing now
#1554 (comment)

For me, it's an uncommon workflow, and somehow invalid one. But OK, it's clearer.