Skip to content

Lift deprecated and alerts attributes into odoc tags#828

Merged
jonludlam merged 4 commits intoocaml:masterfrom
panglesd:deprecated-attr
Feb 24, 2022
Merged

Lift `deprecated` and `alerts` attributes into odoc tags#828
jonludlam merged 4 commits intoocaml:masterfrom
panglesd:deprecated-attr

Commits

Commits on Feb 23, 2022