Makefile: use bash as shell

Depending no the system, sh is the default shell. This has disadvantages when trying to use certain features later. Hence, switch the default to bash. Signed-off-by: Norbert Manthey <[email protected]>
KernelTestFramework · Nov 25, 2020 · 0d6703c · 0d6703c
1 parent 9ab8818
commit 0d6703c
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -22,6 +22,7 @@ LD := ld
 
 NM := nm
 PYTHON := python
+SHELL := bash
 
 GRUB_FILE := grub-file
 GRUB_MKIMAGE := grub-mkimage