On 2015-01-15 08:01, David Holmes wrote:
If the build-dev guys confirm we already assume bash that is fine.
For the rest of the world, we only use bash. For hotspot, we will use bash if called from the top-level Makefile. I can't say anything about what the convention have been for calling the hotspot makefiles directly, though.
/Magnus
