Manually merge changes from Min

because Github decided to start being completely useless and make
merges impossible by in general not working at all