From 085104944b2957f4269fcbfaf0d1874ab0c9ce84 Mon Sep 17 00:00:00 2001 From: Valentin Gagarin Date: Wed, 21 Jun 2023 09:46:23 +0200 Subject: [PATCH] add redirects to changed anchors --- doc/manual/redirects.js | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/doc/manual/redirects.js b/doc/manual/redirects.js index 5cd6fdea2..6813dc6d6 100644 --- a/doc/manual/redirects.js +++ b/doc/manual/redirects.js @@ -342,6 +342,10 @@ const redirects = { "installation/installing-binary.html": { "uninstalling": "uninstall.html" } + "contributing/hacking.html": { + "nix-with-flakes": "#building-nix-with-flakes" + "classic-nix": "#building-nix" + } }; // the following code matches the current page's URL against the set of redirects.