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.

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

add CODEOWNERS for stdpp and iris package directories #2258

Merged
merged 1 commit into from
Aug 18, 2022

Conversation

palmskog
Copy link
Collaborator

Based on the discussion in #2256, ping @RalfJung.

@robbertkrebbers can you please confirm you also want to be reviewer/approver for these Iris and Stdpp packages? Then, we will give you write access to the repo.

@RalfJung
Copy link
Contributor

RalfJung commented Aug 18, 2022

Robbert is on vacation for a few weeks, not sure if he will reply. He doesn't have much oapm experience either. I named him just to make sure that if in doubt, we are not blocked on me (e.g. when I am traveling).

But you said anyway that after a few days of silence from my side you'd go ahead with merging things, so if we follow that protocol, maybe having one Iris team member listed is enough?

@palmskog
Copy link
Collaborator Author

@RalfJung OK, then let's say it's just you in CODEOWNERS for now.

@palmskog palmskog force-pushed the codeowners-iris-stdpp branch from 3faa85a to edfaeb3 Compare August 18, 2022 14:05
Copy link
Contributor

@RalfJung RalfJung left a comment

Choose a reason for hiding this comment

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

Looks good!

@palmskog palmskog merged commit e20eaa9 into coq:master Aug 18, 2022
@palmskog palmskog deleted the codeowners-iris-stdpp branch August 18, 2022 14:16
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants