fe3d137ce
Turns out the issue that led me to push a broken commit in the first place also caused the build to succeed when I tested the fix in a rush. I should've just used the GitHub merge button. Sorry for the noise, hopefully won't happen again.
This fixes 8627656. I accidentally merged an old version to master, sorry for the intermittent breakage.
8627656