Figure out how to update the docs on readthedocs.io

[RalfJung]

Figure out how to update the docs on readthedocs.io

[mitar]

Make an username there and I can add you as an admin. And then you can check out.

[RalfJung]

I created an account, username RalfJung.

[mitar]

Added.

[RalfJung]

Thanks!

There seems to be a way to use webhooks to do the update automatically: https://docs.readthedocs.io/en/stable/webhooks.html

But it seems you used something more manual? Why that?

[mitar]

What manual? It should be on GitHub push to master branch. It is not? What other manual process is there?

Maybe there were some issues compiling things. Sometimes dependencies are not available there, like binary ones. But I think one can mock them or something. Anyway, feel free to try. I do not remember how we had it or why we had it like that.

[RalfJung]

It should be on GitHub push to master branch. It is not?

If that was the case then why did I have to do anything? Once I pressed the "build" button there, the docs got updated, but I had to manually do that.

[mitar]

I do not know. Sometimes hooks have to be re-created because keys expire and stuff like that.

[RalfJung]

I think I've set up a webhook now; we'll see with the next PR if that worked.

[lynxis]

hi @RalfJung does it work for you? Can we close the issue?

[RalfJung]

Yeah, looks like the change in dab746c was reflected on https://tunneldigger.readthedocs.io/en/latest/server.html. :)