Just delete it again. 😄

I believe the problem is that the docs build job doesn't remove deleted pages. I'll ask infra to manually remove it and also the patch.html page.

OK, https://docs.python.org/devguide/faq.html and https://docs.python.org/devguide/patch.html are now gone; you might need to refresh your browser to get the 404.

It might make sense to turn this issue into a request to get the docsbuild script to remove deleted pages when updating the on-line html (if such an issue does not already exist; this isn't the first time something like this has happened).

python/core-workflow#4 is about moving the devguide to Read the Docs and then adding a subdomain on python.org for the devguide. That would alleviate the custom infrastructure dependency.

The problem with deleted pages isn't limited to the devguide. It affects all docs builds.

Thanks @ned-deily
I'm not familiar with docsbuild script. Do you mean that the issue is something to be reported to https://github.com/sphinx-doc/sphinx/ ? If so, I will file a bug there :)

btw I just checked https://docs.python.org/devguide/faq.html and https://docs.python.org/devguide/patch.html both are still active. Could there be caching issue?

@Mariatta See https://github.com/python/docsbuild-scripts for the script that triggers the builds of everything on docs.python.org.

Aha! Thanks @zware will check it out :)

Grrr! They were deleted yesterday but I think the files came back because they also need to be deleted from the docs build directory that probably just gets copied over to the directory from which they are served (I don't have read access to the build directory). I've asked the admins to remove both sets. Hopefully, that will make them permanently go away.

The two pages are now gone again, with luck they will stay that way this time. Since you've opened the issue under docsbuild-scripts, I guess we can close this one?

Sounds good :)