Use bash shell for make#2

Open

jpmeijers wants to merge 1 commit intoaureleq:masterfrom

jpmeijers:master

Commits on Jun 15, 2022

Use bash shell for make, otherwise under Ubuntu dash is used, and one gets a "/bin/sh: 1: Bad substitution" error
jpmeijers
committed