diff options
| -rwxr-xr-x | build_tools/build_documentation.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/build_tools/build_documentation.sh b/build_tools/build_documentation.sh index 2705898e..77eaad68 100755 --- a/build_tools/build_documentation.sh +++ b/build_tools/build_documentation.sh @@ -68,6 +68,12 @@ if test -z "$DOXYGENPATH"; then exit 0 fi +# Check we have the lexicon filter +if test -z "$INPUT_FILTER"; then + echo >&2 "Lexicon filter is not available. Continuing without." + INPUTFILTER='' +fi + # Determine where our output should go if ! mkdir -p "${OUTPUTDIR}" ; then echo "Could not create output directory '${OUTPUTDIR}'" |