Skip to content

misc: Add check for PR names#181

Merged
tachikoma-li merged 2 commits intomasterfrom
gitlint
Apr 20, 2021
Merged

misc: Add check for PR names#181
tachikoma-li merged 2 commits intomasterfrom
gitlint

Conversation

@tachikoma-li
Copy link
Member

@tachikoma-li tachikoma-li commented Apr 14, 2021

To ensure we have consistent PR names as discussed in #179

@tachikoma-li tachikoma-li marked this pull request as ready for review April 14, 2021 02:43
@tachikoma-li tachikoma-li requested review from a team and removed request for a team April 14, 2021 02:43
@tachikoma-li tachikoma-li changed the title gitlint misc: Add check for PR names Apr 14, 2021
@tachikoma-li tachikoma-li changed the title misc: Add check for PR names mis: Add check for PR names Apr 14, 2021
@tachikoma-li tachikoma-li changed the title mis: Add check for PR names misc: Add check for PR names Apr 14, 2021
Copy link
Member

@leoadec leoadec left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'm okay with this, but I'll let @cfarrend decide on the strategy he prefers for adopting gitlint across the repos.

@tachikoma-li
Copy link
Member Author

I'm okay with this, but I'll let @cfarrend decide on the strategy he prefers for adopting gitlint across the repos.

ah, true, I forgot that part. If there is already a plan about applying gitlint across all repos, I am happy to close the PR.

@leoadec
Copy link
Member

leoadec commented Apr 14, 2021

@tachikoma-li I'm not sure if we already have a plan, but devops have been thinking about it, so they might be the best to advise on which approach will be easier to maintain in the future.

@tachikoma-li
Copy link
Member Author

tachikoma-li commented Apr 20, 2021

@tachikoma-li I'm not sure if we already have a plan, but devops have been thinking about it, so they might be the best to advise on which approach will be easier to maintain in the future.

I guess I'll merge this one for now. We can revise it once dev has a better way to consistently manage this issue across repos. @leoadec

@tachikoma-li tachikoma-li merged commit 5628d74 into master Apr 20, 2021
@tachikoma-li tachikoma-li deleted the gitlint branch April 20, 2021 05:27
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Development

Successfully merging this pull request may close these issues.

2 participants