Merged! And I've updated the links to the new URL.
I realize that this means that we no longer load resources (CSS, JS…)
from Google's servers, especially Google Code's, which is an added
benefit from this migration.
Let me know if you see anything to improve on.
PS1: I see that GitHub handles redirections using an HTTP/200 and the
HTML http-equiv meta, which is kind of unfortunate since an HTTP/301
would have been (IMHO) cleaner… Let's say people won't arrive on
/docs/ anyway, now.
PS2: Also, there's the old /doc/ subdirectory of the shedskin
repository which we could maybe remove now that we have the /docs/
subdirectory with all the documentation in it. If someone has an idea
of what we should keep from it… (maybe the man generation?)
PS3: I just remember that we still have to migrate the FOD (frequently
occuring discussions), MSVC, Release Notes and Easy Tasks pages from
the Google Code wiki. While Easy Tasks naturally belongs to GitHub
issues (see #220¹), we might want to put the other pages in the
documentation on ReadTheDocs rather than on the website on GitHub.io
like I initially thought…