tree 1490b66ac8968ec4ec6dbf699a0001a4903c90c3
parent 752bb6ddd4afa03b9bc75202c2dfa0afec353355
author Marcin Czech <maczech@gmail.com> 1599224574 +0200
committer Marcin Czech <maczech@gmail.com> 1599224574 +0200

Use /bin/bash shell instead /bin/sh for make

By default on all linux based systems make uses /bin/sh as a shell.
Switching to /bin/bash allows to use all features provided by /bin/bash
shell

Bug: Issue Issue 13352
Change-Id: I8a02b0be0f83705352bf602ee81cf348c4185c32