tree d76c21cca5fe1177b90f5b9167c9da3435ffaee3
parent ba22fba457d9c72316168102b681de304d4d5dd9
author David Brazdil <dbrazdil@google.com> 1629707703 +0000
committer David Brazdil <dbrazdil@google.com> 1629907556 +0000

Makefile: Use Bash as Make shell

The default is /bin/sh which can differ among individual workstations.
Explicitly pick Bash to avoid compatibility issues and allow using its
non-POSIX features.

Bug: 193407077
Test: make test
Change-Id: I6832c3e5da774d98952ff82c13c95cb320b7ae8f