This reverts commit bdba2dd000f030b1dce3d2bc6caef84929438679 (PR #4610). I don't understand why it was removed in the first place, and didn't get an answer on IRC when I inquired a week ago. But since the commit message states "no-one cares about" the option, it seems reasonable to restore it so long as it is cared about.
Note: This needs adapting if #5833 gets merged first. git will NOT detect the conflict.
