aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xbuild2
1 files changed, 1 insertions, 1 deletions
diff --git a/build b/build
index 9e78fa8..9e57afa 100755
--- a/build
+++ b/build
@@ -128,7 +128,7 @@ main() {
# Generate htmldocs
command -v makeinfo && {
git submodule update --init --remote -f
- make -s -C texidocs DESTDIR="$PWD/src/docs" htmldocs
+ make -s -C texidocs HTMLDIR="$PWD/src/docs" htmldocs
}
# Generate pages