Editorial: use step labels rather than numbers to refer to steps#2052

Merged

ljharb merged 1 commit intomasterfrom step-labels

Jun 19, 2020

+127-127

Commits on Jun 19, 2020

Editorial: use step labels rather than numbers to refer to steps (#2052 )

bakkot
authored and
ljharb
committed