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(-)
(limited to 'build')
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