Skip to content

Conversation

@minad
Copy link
Member

@minad minad commented Nov 5, 2019

missed this when we did the big renaming

@minad minad requested a review from sjaeckel November 5, 2019 19:43
@minad minad added the finished label Nov 5, 2019
@sjaeckel sjaeckel merged commit 67e1816 into develop Nov 5, 2019
@sjaeckel sjaeckel deleted the fix-def-gen branch November 5, 2019 22:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants