Skip to content

Make Jsx.element a private empty record to avoid unnecessary Primitive_option.some#7450

Merged
cknitt merged 7 commits intomasterfrom
jsx-element-private-empty-record
May 9, 2025
Merged

Make Jsx.element a private empty record to avoid unnecessary Primitive_option.some#7450
cknitt merged 7 commits intomasterfrom
jsx-element-private-empty-record

Commits

Commits on May 9, 2025