Commit ef07da5b8cdd00a0d20cd5447793d2f579af018a

nijtmans 2019-03-28T16:13:37

mp_min_u32 is not used anywhere anymore, so it can be removed