Skip to content

fix comment on PlaceMention semantics#129355

Merged
bors merged 1 commit intorust-lang:masterfrom
RalfJung:PlaceMention
Aug 21, 2024
Merged

fix comment on PlaceMention semantics#129355
bors merged 1 commit intorust-lang:masterfrom
RalfJung:PlaceMention

Commits

Commits on Aug 21, 2024