Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Disable most documentation notifications on GitHub
Previously, the documentation comment on GitHub would be removed and then recreated which creates notification emails and to some feels like it's polluting their GitHub inbox. Here, we change this behavior so that only the initial build of the documentation causes such a notification. Further updates to the documentation, do update the links in the comment but do not trigger a notification. This is meant as an alternative to sagemath#37387. See sagemath#37739 for futher ideas about a smarter behavior here.
- Loading branch information