This only includes redirects for user documentation;
external links to the developer documentation would be broken,
but I don't think there are any such link and I don't want to
clutter the file tree unnecessarily.