[anneal] Don't copy Lean deps into build dir#3338

joshlf wants to merge 1 commit into

maingoogle/zerocopy:mainfrom

Gcjwfza3isfk5t3pb32zvwm5hps6nqkhlgoogle/zerocopy:Gcjwfza3isfk5t3pb32zvwm5hps6nqkhlCopy head branch name to clipboard