[PATCH 7/7] make.sh: Fixes Bug#13076