Jeremy Anderson Wed, 18 Feb 2015 08:39:31 -0800
This is NOT a bug in Make -- it is instead a difference in Debian vs. RHEL -- RHEL aliases /bin/sh to /bin/bash, while Debian aliases /bin/sh to /bin/dash.
Please accept my apologies for the spurious report. Thank you, Jeremy