Skip to content

Move Dotty documentation to a separate repository #3236

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.

Sign up for GitHub

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

Jump to bottom
Closed
allanrenucci opened this issue Oct 3, 2017 · 4 comments
Closed

Move Dotty documentation to a separate repository #3236

allanrenucci opened this issue Oct 3, 2017 · 4 comments
Assignees
@allanrenucci
Labels
area:infrastructure exp:intermediate itype:enhancement prio:low

Comments

@allanrenucci
Copy link
Contributor

No description provided.

@allanrenucci allanrenucci self-assigned this Oct 3, 2017
@Blaisorblade
Copy link
Contributor

Blaisorblade commented Feb 13, 2018 •
edited
Loading

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.

Blaisorblade added a commit to dotty-staging/dotty that referenced this issue Feb 14, 2018
@Blaisorblade
Document how to clone dotty faster
21b279b 
Workaround for consequences of scala#3236, probably to revert when that issue is
fixed.
@Blaisorblade Blaisorblade mentioned this issue Feb 14, 2018
Merged
@SzymonPajzert
Copy link
Contributor

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

@Blaisorblade
Copy link
Contributor

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 allanrenucci mentioned this issue Oct 12, 2018
Closed
@allanrenucci
Copy link
Contributor Author

Fixed in #5264

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@allanrenucci allanrenucci

Labels
area:infrastructure exp:intermediate itype:enhancement prio:low
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@Blaisorblade @allanrenucci @SzymonPajzert