Re: [PATCH] Documentation: remove redundant contributing page

[Valentin Gagarin <valentin@gagarin.work>]

> I'd prefer to handle the redirects in nginx config if that's okay with
> you, so it's a proper server-side redirect.

The plugin generates a `_site/redirects.json` file that you can already 
feed to the web server.  It's already enough to have to keep track of 
those redirects manually at all.  You shouldn't have another layer of 
manual work on top.

> Are we adopting FileCopyrightText then License-Identifier as the
> official style, then?  I'll do it across the board if so — if it's
> important enough to rearrange, we should be doing it consistently.

I think we should, but we could just do it lazily, when we touch those 
parts.  But if that produces too much diff noise, feel free not to pick 
the reordering and do a separate bulk change.

> 
>> -    <li><a href="contributing.html">Contributing to Spectrum</a>
>> +    <li><a href="doc/contributing/index.html">Contributing to Spectrum</a>
> 
> doc/contributing is nicer, no?

I don't have an opinion there, but if you want that, it should be 
`doc/contributing/` to avoid the permanent redirect on first access.