Skip to content

Move the gh-pages branch to a separate repository #5248

Closed
@smarter

Description

@smarter

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.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions