From 7d37aff7d4b7687efaaadf64003f4f4ab7d43097 Mon Sep 17 00:00:00 2001
From: Cem Keylan <cem@ckyln.com>
Date: Tue, 15 Sep 2020 11:44:19 +0300
Subject: build: rename DESTDIR to HTMLDIR

---
 build | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3