From 517c547dec086f6332292332571d05dd1cbb6f4b Mon Sep 17 00:00:00 2001 From: Valentin Gagarin Date: Fri, 6 Oct 2023 23:34:08 +0200 Subject: [PATCH] remove duplicate redirects entry --- doc/manual/redirects.js | 1 - 1 file changed, 1 deletion(-) diff --git a/doc/manual/redirects.js b/doc/manual/redirects.js index b2fad19bb76..9d083a43d5b 100644 --- a/doc/manual/redirects.js +++ b/doc/manual/redirects.js @@ -336,7 +336,6 @@ const redirects = { "simple-values": "#primitives", "lists": "#list", "strings": "#string", - "lists": "#list", "attribute-sets": "#attribute-set", }, "installation/installing-binary.html": {