From 7d37aff7d4b7687efaaadf64003f4f4ab7d43097 Mon Sep 17 00:00:00 2001 From: Cem Keylan 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