From e296e9667e0ea50004cce63021dfb7f69465367d Mon Sep 17 00:00:00 2001
From: Arthur Meyre <arthur.meyre@zama.ai>
Date: Wed, 11 Aug 2021 09:42:31 +0200
Subject: [PATCH] chore(tools): use /bin/bash as shell for the Makefile

- tested some commands with an environment which had /bin/sh as default
shell, some did not work, this fixes it
---
 Makefile | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Makefile b/Makefile
index 855351dc8..04557f95f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,3 +1,5 @@
+SHELL:=/bin/bash
+
 setup_env:
 	poetry install
 	poetry run python -m pip install -U pip wheel setuptools