Skip to content

Conversation

@fingolfin
Copy link
Member

Resolves #50351 albeit with a bit of a hack.

Current:
Screenshot 2025-11-17 at 14 51 36

With this patch:
Screenshot 2025-11-17 at 14 52 11

I deliberately left "The Julia REPL" alone (so it is still sorted under "REPL") as that felt more natural to me compared to sorting it under "Julia" but obviously this could easily be changed as well.

@fingolfin fingolfin added the docs This change adds or pertains to documentation label Nov 17, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

docs This change adds or pertains to documentation

Projects

None yet

Development

Successfully merging this pull request may close these issues.

List of stdlibs in the docs is sorted awkwardly

2 participants