-
Notifications
You must be signed in to change notification settings - Fork 1.1k
Move the gh-pages branch to a separate repository #5248
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Labels
Comments
@allanrenucci Can I assign you to this one ? |
It took me 36 minutes to clean clone the dotty repo and the directory weighs 609 MB |
Sure |
Duplicate of #3236 |
allanrenucci
added a commit
to dotty-staging/dotty
that referenced
this issue
Oct 16, 2018
allanrenucci
added a commit
to dotty-staging/dotty
that referenced
this issue
Oct 16, 2018
allanrenucci
added a commit
to dotty-staging/dotty
that referenced
this issue
Oct 16, 2018
allanrenucci
added a commit
to dotty-staging/dotty
that referenced
this issue
Oct 16, 2018
allanrenucci
added a commit
that referenced
this issue
Oct 26, 2018
Fix #5248: Move generated doc to lampepfl/dotty-website
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Cloning the dotty repository is getting harder and harder because it keeps growing, and a big factor in that growth seems to be https://github.com/lampepfl/dotty/tree/gh-pages, instead of using a branch in the main repository we should use a separate repo for this.
The text was updated successfully, but these errors were encountered: