Skip to content

Revert 'Rename profile=user to profile=dist' - #112886

Merged
bors merged 1 commit into
rust-lang:masterfrom
clubby789:revert-user-dist
Jun 21, 2023
Merged

Revert 'Rename profile=user to profile=dist'#112886
bors merged 1 commit into
rust-lang:masterfrom
clubby789:revert-user-dist

Revert 'Rename profile=user to profile=dist'

e3e65d1
Select commit
Loading
Failed to load commit list.

Workflow runs completed with no jobs