Skip to content
This repository has been archived by the owner on Feb 24, 2020. It is now read-only.

maintainers: update #3935

Merged
merged 1 commit into from Aug 2, 2018
Merged

maintainers: update #3935

merged 1 commit into from Aug 2, 2018

Conversation

lucab
Copy link
Member

@lucab lucab commented May 28, 2018

This updates the maintainers list to current reality.

@lucab
Copy link
Member Author

lucab commented May 28, 2018 •
edited

I'll abuse this to also ping people who still have access, but it could be worth a confirmation:

/cc @alban @iaguis

@krnowak
Copy link
Collaborator

krnowak commented Jun 6, 2018

Pong.

Who's going to handle issues in the damn build system if I'm gone? ;)

iaguis
iaguis approved these changes Aug 2, 2018
View reviewed changes
Copy link
Member

@iaguis iaguis left a comment

Choose a reason for hiding this comment

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

Thanks! Let's merge this for now, if @yifan-gu and @dgonyeo want to be removed they can file another PR.

@iaguis iaguis merged commit 03285a7 into rkt:master Aug 2, 2018
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@iaguis iaguis iaguis approved these changes

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

Successfully merging this pull request may close these issues.

None yet
3 participants
@lucab @krnowak @iaguis