CI: Assign milestone on merged PRs

[echoix]

Addresses #4398 (comment)

This PR assigns a milestone when a PR is closed if none is set, using pull_request_target trigger with closed activity type. It uses up an API call to know if the PR has a milestone set (limit is 5000 per hour when authenticated). If I used the info from the github event context, the information is populated when the job is queued, and will maybe not represent the state once it will run, and will keep the old state if a rerun is made. I tried to use the gh cli instead of their javascript action's ecosystem so steps could be reproduced locally too using the same gh cli calls.

If there are no milestones for that PR, then it uses a second API call to fetch the include/VERSION file at the ref of the merged result (so pull_request_target doesn't matter here, it is still up-to-date). It parses that file like for the coverity scan workflow, but also removes "dev" and "RC" followed by 0 or more numbers. This builds the milestone title to apply, using a third API call.

Using the VERSION file allows it to keep working on newer and older versions (working on older branches if the workflow is backported)

Known limitations:

• No attempt is made to try to prevent running on forks that merges PRs in their forks: This also allows to change the repo's name and organization in the future without having to change release branches.
• No attempt to create a milestone if it doesn't exist: this workflow will simply fail, as the gh cli will say that the milestone doesn't exist. As it might only happen once or twice during a year (assuming the milestone wasn't set on the PR already), I didn't take more time to do it. In part because running on PR merges doesn't have a lot of visibility (doesn't show on the pushed commit on main checks for example), and what dates and description should be set? That's more of a manual thing to do.