From e40122c0b5ae4dfae0958163b2ff1dc3f25d5845 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Sat, 3 Mar 2018 13:08:35 +0100
Subject: [PATCH] Make: use bash

---
 Makefile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Makefile b/Makefile
index 6267dcb..e49826d 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,6 @@
 WHOLE=whole
 LAST=last
+SHELL:=/bin/bash
 
 HEADER=header.tex