| commit | 94acb6f3cb9e7011a01d5a1679bdb88df6b93df7 | [log] [tgz] |
|---|---|---|
| author | David Brazdil <dbrazdil@google.com> | Mon Aug 23 08:35:03 2021 +0000 |
| committer | David Brazdil <dbrazdil@google.com> | Wed Aug 25 16:05:56 2021 +0000 |
| tree | d76c21cca5fe1177b90f5b9167c9da3435ffaee3 | |
| parent | ba22fba457d9c72316168102b681de304d4d5dd9 [diff] |
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
diff --git a/Makefile b/Makefile index f35f896..e640557 100644 --- a/Makefile +++ b/Makefile
@@ -16,6 +16,7 @@ CPUS ?= $(shell nproc) MAKEFLAGS += --jobs=$(CPUS) +SHELL ?= $(shell which bash) ## ## Folders