diff options
author | github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com> | 2024-02-07 11:44:06 +0100 |
---|---|---|
committer | GitHub <noreply@github.com> | 2024-02-07 11:44:06 +0100 |
commit | 2db5c5326bb1c7ed11321be4bfd64b201b74320a (patch) | |
tree | 48f06593b844a672048594cb9b9383432f1d4777 /doc/manual | |
parent | 5f7f68e0a820ee4ca85820d4facaa50678f42052 (diff) |
fix location of `_redirects` file (#9956)
Diffstat (limited to 'doc/manual')
-rw-r--r-- | doc/manual/src/_redirects (renamed from doc/manual/_redirects) | 0 |
1 files changed, 0 insertions, 0 deletions
diff --git a/doc/manual/_redirects b/doc/manual/src/_redirects index 4ea289d86..4ea289d86 100644 --- a/doc/manual/_redirects +++ b/doc/manual/src/_redirects |