Join GitHub today
GitHub is home to over 40 million developers working together to host and review code, manage projects, and build software together.Sign up
alex: drop patch #73693
simonmar/alex#140 was merged and the patch has been applied in alex
Motivation for this change
Build is currently broken:
I've confirmed that this fixed the alex build, so I'm merging in.
@peti I'm merging this in even though it is to the