Stream: cranelift

Topic: readthedocs site


view this post on Zulip Dan Gohman (Mar 15 2021 at 15:48):

I have admin access to the cranelift.readthedocs.io site. Would it make sense to simply delete the site?

view this post on Zulip Chris Fallin (Mar 15 2021 at 15:50):

Would there be a way to make it redirect to the new location? (doesn't seem like a huge deal, but just in case anyone has an old link)

view this post on Zulip Dan Gohman (Mar 15 2021 at 15:52):

I'm looking at the readthedocs admin panel and trying to figure out what it can do

view this post on Zulip Benjamin Bouvier (Mar 15 2021 at 15:54):

Ah yeah, if there was a way to just do an HTTP redirect, it would probably be ideal!

view this post on Zulip Dan Gohman (Mar 15 2021 at 15:56):

I added a Redirect in the Redirect page, but it didn't do anything. I think the whole thing needs us to migrate off of Github webhooks

view this post on Zulip Dan Gohman (Mar 15 2021 at 15:56):

Anyone want to create a readthedocs account and become an admin?

view this post on Zulip Dan Gohman (Mar 15 2021 at 15:56):

:smiley:

view this post on Zulip Dan Gohman (Mar 15 2021 at 16:00):

Otherwise I think it's best to just delete the site and update our own docs

view this post on Zulip Chris Fallin (Mar 15 2021 at 16:05):

+1 to just deleting if it's too much hassle; $favorite_search_engine should be pretty good about dropping it from the index then

view this post on Zulip Dan Gohman (Mar 15 2021 at 16:28):

Sounds good, I've now deleted it.


Last updated: Dec 23 2024 at 12:05 UTC