#698 removed the need for the circleci build. I have turned off the circleci webhook so it won't get triggered in the future, but at some point we should probably just delete it so it doesn't confuse some future maintainer.
I don't want to do it now though because we might need to restore it if something goes wrong in the transition. So I think this should wait, say, a month or so just to make sure we don't need it.
(Note only maintainers can do this, so this is mostly just informational to the maintainers.)
#698 removed the need for the circleci build. I have turned off the circleci webhook so it won't get triggered in the future, but at some point we should probably just delete it so it doesn't confuse some future maintainer.
I don't want to do it now though because we might need to restore it if something goes wrong in the transition. So I think this should wait, say, a month or so just to make sure we don't need it.
(Note only maintainers can do this, so this is mostly just informational to the maintainers.)