-
Notifications
You must be signed in to change notification settings - Fork 210
Home
Welcome to the chaos wiki!
Document history here
- Programming language used
- Rules followed by bot
- How many times it died
- Services running
- Add to me
Some things the bot does due to the limitations imposed by github, etc. Others, we can change almost freely
last modified date is impossible even for the api, i've found. you only get access to the "pushed_at" field of the pr's repo which is really bad because the pr's repo's "pushed_at" field gets updated when commits are pushed to it on any branch
This has the interesting effect that you can only have one pr at a time for any user. And there are a few other things that limit the rate at which prs are merged
The length of the voting window is defined here. That's picked up and passed into another function used to check PRs where it's compared to a per-PR duration. That duration is since the PR was lasted updated. "Last updated" is defined in terms of Github API stuff that seems to me to check when the PR was lasted changed. This is also the same value used to reset votes, so the duration and votes reset at the same time.
Check out here for contributing guidelines. Don't have an idea? Try implementing one of these ones!
| Port | Where | What |
|---|---|---|
| 80 | server/server.py |
static site server/index.html
|
| 8081 | nginx static directory server | logs from /var/log/supervisor/
|