Skip to content

Conversation

@bobzhang
Copy link
Member

No description provided.

@bobzhang bobzhang force-pushed the record_label_renaming branch from e131b7e to 769ac67 Compare November 23, 2019 18:48
@bobzhang bobzhang changed the title add Ext_list.find_def record renaming support fix #3949 Nov 23, 2019
@bobzhang bobzhang changed the title record renaming support fix #3949 record renaming support fix #3979 Nov 23, 2019
@bobzhang bobzhang merged commit 04dc4a5 into master Nov 23, 2019
@bobzhang bobzhang deleted the record_label_renaming branch November 23, 2019 19:17
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