Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

PHPORM-190: Update drivers-github-tools to v2 #2998

Merged
merged 1 commit into from
Jun 7, 2024
Merged

PHPORM-190: Update drivers-github-tools to v2 #2998

merged 1 commit into from
Jun 7, 2024

Conversation

alcaeus
Copy link
Member

@alcaeus alcaeus commented Jun 5, 2024

@alcaeus alcaeus requested a review from jmikola June 5, 2024 10:25
@alcaeus alcaeus requested a review from a team as a code owner June 5, 2024 10:25
@github-actions github-actions bot added the github label Jun 5, 2024
jmikola
jmikola approved these changes Jun 7, 2024
View reviewed changes
Copy link
Member

@jmikola jmikola left a comment

Choose a reason for hiding this comment

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

Reminder to look into whatever repository config interrupted the PHPC release yesterday. Worth checking that PHPLIB is also correctly configured, since you merged this there earlier in the week.

@alcaeus
Copy link
Member Author

alcaeus commented Jun 7, 2024

Reminder to look into whatever repository config interrupted the PHPC release yesterday. Worth checking that PHPLIB is also correctly configured, since you merged this there earlier in the week.

Yep, I did so immediately after discovering the problem yesterday 👍

@alcaeus alcaeus merged commit 798a5ba into mongodb:4.4 Jun 7, 2024
26 checks passed
@alcaeus alcaeus deleted the phporm-190-update-drivers-tools-v2 branch June 7, 2024 12:58
@mongodb-php-bot mongodb-php-bot mentioned this pull request Jun 7, 2024
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jmikola jmikola jmikola approved these changes

Assignees
No one assigned
Labels
github
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@alcaeus @jmikola