PR #51411 clean up identifiers defined in `Main`

clean up identifiers defined in `Main` #51411

JeffBezanson merged 1 commit into master from jb/mainnames

vchuravy approved these changes on 2023-09-20

JeffBezanson force pushed from 63342c37 to a47e7964 2 years ago

vtjnash commented on 2023-09-21

clean up identifiers defined in `Main`

3cd2088f

JeffBezanson force pushed from a47e7964 to 3cd2088f 2 years ago

JeffBezanson merged ab94a242 into master 2 years ago

JeffBezanson deleted the jb/mainnames branch 2 years ago

Reviewers

vchuravy

vtjnash

Assignees

No one assigned

Labels

None yet

Milestone

No milestone