From 296ce4be83cb242de9b2c366673ff89c73c4d2cd Mon Sep 17 00:00:00 2001 From: Sergey Matveev Date: Sun, 18 Jul 2021 14:43:30 +0300 Subject: [PATCH] Unnecessary TOP_NODE_UP_URL --- doc/www.do | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/www.do b/doc/www.do index 660e142..79c7e40 100644 --- a/doc/www.do +++ b/doc/www.do @@ -9,7 +9,6 @@ ${MAKEINFO:=makeinfo} --html \ --set-customization-variable FORMAT_MENU=menu \ --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 index.texi -- 2.44.0