PR #18316 [ty] Playground: Better default settings

[ty] Playground: Better default settings #18316

sharkdp merged 1 commit into main from david/playground-default-settings

[ty] Playground: Better default settings

dad5ad09

sharkdp added playground

sharkdp added ty

sharkdp requested a review from

MichaReiser 264 days ago

MichaReiser approved these changes on 2025-05-26

sharkdp merged d51f6940 into main 264 days ago

sharkdp deleted the david/playground-default-settings branch 264 days ago

Reviewers

MichaReiser

Assignees

No one assigned

Labels

playground ty

Milestone

No milestone