On every push that changes relevant files, and periodically, configure the repository's issue and pull request labels
according to the universal, shared, and local label configuration files.
Please check if the PR fulfills these requirements
[x] The PR has no duplicates (please search among the Pull Requests
before creating one)
[ ] Tests for the changes have been added (for bug fixes / features)
What kind of change does this PR introduce?
Infrastructure enhancement
What is the current behavior?
Although the repo uses the standardized repository labels for Arduino tooling projects, they are managed on a per-repo basis and thus require direct manual work to keep in sync.
What is the new behavior?
On every push that changes relevant files, and periodically, use github-label-sync to configure the repository's issue/PR labels according to the universal, shared, and local label configuration files.
On every push that changes relevant files, and periodically, configure the repository's issue and pull request labels according to the universal, shared, and local label configuration files.
Please check if the PR fulfills these requirements
[x] The PR has no duplicates (please search among the Pull Requests before creating one)
[x] The PR follows our contributing guidelines
[ ] Tests for the changes have been added (for bug fixes / features)
What kind of change does this PR introduce?
Infrastructure enhancement
What is the current behavior?
Although the repo uses the standardized repository labels for Arduino tooling projects, they are managed on a per-repo basis and thus require direct manual work to keep in sync.
What is the new behavior?
On every push that changes relevant files, and periodically, use github-label-sync to configure the repository's issue/PR labels according to the universal, shared, and local label configuration files.
Other information:
Preview of the changes that would result from merging this PR: https://github.com/arduino/arduino-language-server/pull/82/checks?check_run_id=3702677393#step:9:16