make: use /usr/bin/env bash rather than /bin/bash

Tragicus · Aug 21, 2020 · ca13a49 · ca13a49
1 parent 73a1f68
commit ca13a49
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Makefile b/Makefile
@@ -15,7 +15,7 @@ help:
 
 INSTALL=_build/install/default
 BUILD=_build/default
-SHELL:=/bin/bash
+SHELL:=/usr/bin/env bash
 TIMEOUT=90.0
 RUNNERS=\
   dune \