From 89351f896fc98292df0a111222d48d6c275303fa Mon Sep 17 00:00:00 2001 From: Sergey Matveev Date: Tue, 17 Aug 2021 16:24:46 +0300 Subject: [PATCH] Unnecessary TOP_NODE_UP_URL --- www.do | 1 - 1 file changed, 1 deletion(-) diff --git a/www.do b/www.do index 8dbbb22..4d0a83c 100644 --- a/www.do +++ b/www.do @@ -10,7 +10,6 @@ ${MAKEINFO:-makeinfo} --html \ --set-customization-variable EXTRA_HEAD='' \ --set-customization-variable SHOW_TITLE=0 \ --set-customization-variable DATE_IN_HEADER=1 \ - --set-customization-variable TOP_NODE_UP_URL=index.html \ --set-customization-variable CLOSE_QUOTE_SYMBOL=\" \ --set-customization-variable OPEN_QUOTE_SYMBOL=\" \ -o $html www.texi -- 2.44.0