Index: man/src/make_docs.sh |
diff --git a/man/src/make_docs.sh b/man/src/make_docs.sh |
index d011a61229230fda628d4995a324e15982736dff..73d76e248974353fb1b9aa286bf757c9cb15b63e 100755 |
--- a/man/src/make_docs.sh |
+++ b/man/src/make_docs.sh |
@@ -1,4 +1,7 @@ |
-#!/bin/bash -e |
+#!/usr/bin/env bash |
+ |
+set -e |
+ |
shopt -s nullglob |
cd $(dirname "$0") |