summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorChristian Grothoff <christian@grothoff.org>2020-12-28 23:47:01 +0100
committerChristian Grothoff <christian@grothoff.org>2020-12-28 23:47:01 +0100
commit38b2445cbe48df349438c50670cf194544897de6 (patch)
treea54fcfe21efecb31a5f6cb2ddfea8a217b594c70 /doc
parente30fd985fd765ad25505c3d73d35e8535512ed2e (diff)
fix some linting issues
Diffstat (limited to 'doc')
-rwxr-xr-xdoc/man/produce_html.sh.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/man/produce_html.sh.in b/doc/man/produce_html.sh.in
index d2bd768a8..8680c0106 100755
--- a/doc/man/produce_html.sh.in
+++ b/doc/man/produce_html.sh.in
@@ -1,4 +1,4 @@
-#!/bin/sh
+#!/bin/bash
if test -e @PKGDATADIRECTORY@/existence.sh
then