ci: Push labels to PR title [CI🤖]

[daniele-moro]

Based on the labels from .github/labeler.yml add labels to the PR title too.

[Copilot]

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

Comments suppressed due to low confidence (1)

.github/workflows/auto-add-labels.yml:41

• The GitHub CLI command 'gh pr edit' may fail if the CLI is not authenticated. Consider adding a step to authenticate using the provided GH_TOKEN before running this command.

gh pr edit ${{ github.event.pull_request.number }} --title "$new_pr_title"

[Copilot]

Copilot reviewed 2 out of 2 changed files in this pull request and generated no comments.

Comments suppressed due to low confidence (1)

.github/workflows/auto-add-labels.yml:30

• The regex in the sed command may not correctly handle all cases: if the PR title does not strictly conform to the expected '[labels] Title' format, it could result in an empty value. Consider refining the regex or adding additional logic to ensure the title is updated correctly when no initial label prefix is present.

new_pr_title=$(echo "$old_pr_title" | sed -n 's/^\[\([^]]*\)\] *//p')

[cjnolan]

Is the checkout needed?

[daniele-moro]

Not anymore, it was needed for using GH shell. Now that we moved to REST API, that should not be needed anymore. Fixing.

[zdw]

What's the benefit of this, other than having a title? For searching? Does this also affect the commit message that is merged?

If this is across many sub-repos, won't the title be potentially very long, to the point that it runs off the end of the text area for a title into the commit message?

[github-actions]

This pull request is stale because it has been open 30 days with no activity. Make a comment or update the PR to avoid closing PR after 15 days.