Merge postgrest-docs with main repo

[steve-chavez]

Problem

Keeping postgrest-docs in sync with the main repo is quite painful. Duplicate work is done in tagging a release on docs, duplicating the CHANGELOG on docs, etc. This makes us slower overall.

Solution

Merge postgrest-docs with main repo while preserving history. It's possible as previously discussed on: #1897 (comment)

We still need to figure out the steps for CI and readthedocs.

[steve-chavez]

If we only make releases through non-main branches, like we have been doing for some patch/minor versions:

• https://github.com/PostgREST/postgrest/tree/rel-10.1.2
• https://github.com/PostgREST/postgrest/tree/rel-10.2.0
• https://github.com/PostgREST/postgrest/tree/rel-11.2.1

Then we would be compatible with the way we release docs too, which is done exclusively on branches: https://github.com/PostgREST/postgrest-docs/branches

Then our main here would point to the latest docs, which is also done for postgrest-docs.

[steve-chavez]

Since CI for docs is fast, we could run it on every PR.

We would have to drop some old version of the docs though, which don't have equivalent branch releases here.

(Actually no, we can just create the branches)

I think this would be the smoother transition.

[wolfgangwalther]

Is there any idea about how to proceed with all the issues in the postgrest-docs repo, already? It would make the most sense to move them here, but we can't do that 1-by1...

[steve-chavez]

On #1897 (comment)

I think we could still maintain the separate repo for tracking issues, even if we move the docs into the code repo
Benefits
Docs-related issues/PRs separated from other ones

We agreed to keep the docs issues on its own repo. I think we should keep that for now.

[wolfgangwalther]

We agreed to keep the docs issues on its own repo. I think we should keep that for now.

I'm not sure this will work with an archived repo as mentioned in #3113 (comment). I think we should definitely archive the docs repo.

I also don't see the any good reason to keep it that way - except to avoid effort in moving things over. But I don't find that a good reason. I'd rather invest some time to get this right now than to keep having two repos.

It will be really inconvenient to deal with PRs in the main repo solving issues in the docs repo etc...

[laurenceisla]

Yes, I think moving them to core is the best if archiving the docs repo gives problems.

It would make the most sense to move them here, but we can't do that 1-by1...

Someone mentioned that bulk issue migration can be done using GitHub CLI (it doesn't keep the labels though):

https://github.com/orgs/community/discussions/9695#discussioncomment-5423988