Skip to content

Conversation

@sostock
Copy link
Contributor

@sostock sostock commented Jul 30, 2020

This was formerly #36836, which I apparently cannot reopen because I force-pushed it. This implements the “minor change” part of that PR on top of #36850 and should be discussed at triage.

@sostock
Copy link
Contributor Author

sostock commented Jul 31, 2020

Since this is a minor change, should it appear in NEWS.md?

@stevengj
Copy link
Member

stevengj commented Aug 1, 2020

It's not an API change, just an optimization, so no NEWS required.

@StefanKarpinski StefanKarpinski merged commit 1888e31 into JuliaLang:master Aug 2, 2020
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.

3 participants