build: rename DESTDIR to HTMLDIR

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