Merge this one into eclipse.platform repo?

[vogella]

Should be merge this one with the Merge this one into eclipse.platform repo?

cc @laeubi ?

[laeubi]

I think it makes sense to keep this separate as it does not contain any code we usually deliver or depends on the release cycle.

[Bananeweizen]

While I generally prefer having less organizations, that also might have an impact on access rights. The move of "news" already made people of non-platform projects suddenly not being able to commit news entries on their own. We should avoid a similar situation for the user guide, and prefer easy contribution over less orgs here. If the restricted access issue can be avoided by some other means, then of course my argument might not be an issue at all.

[laeubi]

@Bananeweizen this is already included in the eclipse-platform organization, but @vogella asked to merge this into the eclipse.platform repository inside the organization.

[Bananeweizen]

Thanks for clarifying, I completely missed that. In that case I vote against merging. Having one repository with multiple different builds is a nightmare. Right now the build of the documentation takes around 10 seconds on my local machine and you don't need to know anything about "outside things". It doesn't have a parent POM etc..

If this were merged, that fast build would be gone, or the github actions and similar stuff would have to become way more complicated to differentiate between "a full platform build" and "a documentation only build".