diff options
Diffstat (limited to 'publish-docs')
| -rwxr-xr-x | publish-docs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/publish-docs b/publish-docs index ab0622a..dc39eb3 100755 --- a/publish-docs +++ b/publish-docs @@ -6,7 +6,7 @@ build_docs() { local srcdir="$1" local log="$(mktemp)" - + set -eu cd "$srcdir"/doc if make dirhtml > "$log" 2>&1 |