From 2d74b56aee84051d386f124c092d143b9cc437f9 Mon Sep 17 00:00:00 2001
From: Valentin Gagarin <valentin.gagarin@tweag.io>
Date: Tue, 6 Feb 2024 23:22:34 +0100
Subject: [PATCH] fix location of `_redirects` file

the Netlify `_redirects` file must be in the root directory [0] of the
files to serve, and mdBook copies all the files in `src` that aren't
`.md` to the output directory [1].

[0]: https://docs.netlify.com/routing/redirects/
[1]: https://rust-lang.github.io/mdBook/guide/creating.html#source-files
---
 doc/manual/{ => src}/_redirects | 0
 1 file changed, 0 insertions(+), 0 deletions(-)
 rename doc/manual/{ => src}/_redirects (100%)

diff --git a/doc/manual/_redirects b/doc/manual/src/_redirects
similarity index 100%
rename from doc/manual/_redirects
rename to doc/manual/src/_redirects