Skip to content
This repository has been archived by the owner on Apr 26, 2024. It is now read-only.

extra_users is actually a list of UserIDs #2982

Merged
merged 1 commit into from
Mar 13, 2018

Conversation

erikjohnston
Copy link
Member

No description provided.

Copy link
Member

@richvdh richvdh left a comment

Choose a reason for hiding this comment

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

lgtm

@richvdh richvdh assigned erikjohnston and unassigned richvdh Mar 13, 2018
@erikjohnston erikjohnston merged commit c82111a into develop Mar 13, 2018
@erikjohnston erikjohnston deleted the erikj/fix_extra_users branch March 22, 2018 13:00
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants