From 33368b7e5cca1600e908e1f780595abea840ca7d Mon Sep 17 00:00:00 2001
From: Holger Weiss <holger@zedat.fu-berlin.de>
Date: Thu, 24 Jul 2014 15:15:00 +0200
Subject: [PATCH] doc/Makefile: Don't insist on using /bin/bash

Fix "make doc" for systems that don't have /bin/bash.  There's no
bash-specific code in doc/Makefile anymore.
---
 doc/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/Makefile b/doc/Makefile
index db378be67..a67148798 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -1,6 +1,6 @@
 # $Id$
 
-SHELL = /bin/bash
+SHELL = /bin/sh
 
 CONTRIBUTED_MODULES = ""
 #ifeq ($(shell ls mod_http_bind.tex),mod_http_bind.tex)