Move Dotty documentation to a separate repository

[allanrenucci]

[Blaisorblade]

We figured out the gh-pages branch might slow down cloning this repo. git init; git remote add origin https://github.com/lampepfl/dotty.git; git pull origin master seems a workaround for now.

EDIT: Better workaround is git clone --recursive --single-branch https://github.com/lampepfl/dotty.git.

[SzymonPajzert]

Is this issue still requested given that we can clone just single branch?

[Blaisorblade]

It’s still low priority. You can usually clone a repo without special instructions. But I fear this can’t be fixed externally since some of the code involved with publishing docs isn’t available externally.

[allanrenucci]

Fixed in #5264