Merge pull request #637 from lameiro/master

Specify /bin/bash for the Makefile, as some distros may have other shells as /bin/sh

Makefile

+SHELL := /bin/bash
+
 # prints variables for debugging
 print-%: ; @echo $($*)