diff options
| -rwxr-xr-x | doxygen/build_man.sh | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/doxygen/build_man.sh b/doxygen/build_man.sh index c68876c..0d3be4c 100755 --- a/doxygen/build_man.sh +++ b/doxygen/build_man.sh @@ -1,4 +1,5 @@ -#!/bin/bash -p +#!/bin/sh +[ -n "$BASH" ] || exec bash -p $0 # Script to process man pages output by doxygen. # We need to use bash for its associative array facility. |