Dan Gohman (Mar 15 2021 at 15:48): 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?
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)
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
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!
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
Dan Gohman (Mar 15 2021 at 15:56):Anyone want to create a readthedocs account and become an admin?
Dan Gohman (Mar 15 2021 at 15:56)::smiley:
Dan Gohman (Mar 15 2021 at 16:00):Otherwise I think it's best to just delete the site and update our own docs
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
Dan Gohman (Mar 15 2021 at 16:28):Sounds good, I've now deleted it.
Last updated: Nov 22 2024 at 16:03 UTC