Skip to content
This repository was archived by the owner on Jan 12, 2024. It is now read-only.

Renamed 'Concretion' to 'Concretization' #398

Closed
ScottCarda-MS wants to merge 1 commit into from
Closed

Renamed 'Concretion' to 'Concretization' #398

ScottCarda-MS wants to merge 1 commit into from

Conversation

@ScottCarda-MS
Copy link
Contributor

@ScottCarda-MS ScottCarda-MS commented Apr 9, 2020

No description provided.

@microsoft-github-updates microsoft-github-updates bot changed the base branch from master to main September 9, 2020 07:51
@bettinaheim
Copy link
Contributor

bettinaheim commented Oct 9, 2020

@ScottCarda-MS Can we close this PR? It would be nice to do this renaming to use consistent terminology, but I think it is easier to do it on the current version rather than resolve the conflicts here. Could you set up a new PR for that?

@ScottCarda-MS
Copy link
Contributor Author

ScottCarda-MS commented Oct 9, 2020

@ScottCarda-MS Can we close this PR? It would be nice to do this renaming to use consistent terminology, but I think it is easier to do it on the current version rather than resolve the conflicts here. Could you set up a new PR for that?

The intension was to address this after the call graph was implemented into master. You are right in that it will need to be redone with the current version rather than here. I'd like to keep this up as a reminder to myself until #654 is completed, after which I will create a new PR.

@ScottCarda-MS
Copy link
Contributor Author

ScottCarda-MS commented Oct 16, 2020

Closing this in favor of #682

@ScottCarda-MS ScottCarda-MS deleted the sccarda/RenameConcretionToConcretization branch October 17, 2020 00:49
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@ScottCarda-MS @bettinaheim