bug#37808
"make_binary_distribution" does not always generate correct names

Successfully tested on 5.1 sources.