Fix src/etc/pre-push.sh when build.locked-deps is already set#112146
Merged
bors merged 1 commit intorust-lang:masterfrom Jun 2, 2023
src/etc/pre-push.sh when build.locked-deps is already set#112146