From b6eefffb64cb62671a15281ed0a572a227e56c55 Mon Sep 17 00:00:00 2001
From: Florian Loitsch <florian@toit.io>
Date: Wed, 19 Jul 2023 18:37:52 +0200
Subject: [PATCH] Use bash.

---
 tools/main.toit | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/main.toit b/tools/main.toit
index 941a3a0..eaa77e6 100644
--- a/tools/main.toit
+++ b/tools/main.toit
@@ -200,6 +200,9 @@ create_makefile_ dir/string --toit_root/string --build_path/string --chip/string
   // This doesn't work if the paths '"' characters.
   // Should be pretty rare.
   file.write_content --path="$dir/Makefile" """
+    SHELL := bash
+    .SHELLFLAGS := -eu -o pipefail -c
+
     IDF_PATH := $idf_path
     IDF_PY := \$(IDF_PATH)/tools/idf.py
     TOIT_ROOT := $absolute_toit_root