Expand description
GitHub, once asked in the task settings (docs/github.md): the issues and pull requests that are yours, in the local “GitHub” list every thirty minutes, each in the project whose routes take it; GitHub’s notification mail tied to its task and that task’s project.
Constants§
- EVERY 🔒
- SETTLED 🔒
- GitHub’s search can take a while to see a change: an issue it stopped finding is let go only when nothing changed on it for this long.
Functions§
- bring 🔒
- Brings GitHub’s open issues that are yours into the list, and lets go of those it no longer lists: closed, or no longer yours. Returns how many tasks changed.
- list 🔒
- The “GitHub” list, kept on this computer only.
- start 🔒
- Starts bringing GitHub’s issues when asked; brings them now when running.
- stop 🔒
- Stops it: turned off.
- tie_
mail 🔒 - GitHub’s notification mail, tied to its issue’s task, and to that task’s project. Mail about an issue that is not yours makes nothing; nor does a message that only claims to come from GitHub: its signature must say so, as the Porch judges it, or anyone could slip a message into a project.