Skip to content

Conversation

@jakobnissen
Copy link
Member

@jakobnissen jakobnissen commented Dec 23, 2021

Mention the new feature of #43305 in the manual.
If merged, the "needs docs" label on the parent PR can be removed.

@vchuravy vchuravy added this to the 1.8 milestone Jan 6, 2022
@vtjnash vtjnash merged commit b08d9ee into JuliaLang:master Jan 12, 2022
@jakobnissen jakobnissen deleted the constdocs branch January 12, 2022 19:49
LilithHafner pushed a commit to LilithHafner/julia that referenced this pull request Feb 22, 2022
LilithHafner pushed a commit to LilithHafner/julia that referenced this pull request Mar 8, 2022
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.

4 participants