From e7d51886ef90f5b2d4fa13911381680ac192fc37 Mon Sep 17 00:00:00 2001
From: Mayank Singhal <17mayanksinghal@gmail.com>
Date: Tue, 6 Apr 2021 02:21:18 +0530
Subject: [PATCH] Find bash from PATH instead of /bin/bash

---
 docs/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/docs/Makefile b/docs/Makefile
index ff68bf1ae..87d5d3047 100644
--- a/docs/Makefile
+++ b/docs/Makefile
@@ -8,7 +8,7 @@ PYTHON       = python
 SPHINXOPTS   =
 PAPER        =
 SOURCES      =
-SHELL        = /bin/bash
+SHELL        = /usr/bin/env bash
 
 ALLSPHINXOPTS = -b $(BUILDER) -d build/doctrees \
                 -D latex_elements.papersize=$(PAPER) \