Abort job polling interval

[onlyann]

Closes #1184

Successful PR Checklist:

• Tests
  • (not applicable?)
• Documentation
  • (not applicable?)

PR label(s):

• PR type: breaking 💥 Contains breaking changes
• PR type: feature ⭐️ Contains new features
• PR type: bugfix 🕵️ Contains bug fix
• PR type: miscellaneous 👾 Contains misc changes
• PR type: dependencies 🤖 Contains only dependencies updates
• PR type: documentation 📚 Contains documentation updates

Changes

This adds abort_job_polling_interval to be able to specify a different interval for polling abort requests.
It also renames polling_interval to fetch_job_polling_interval.

[github-actions]

Coverage report

Click to see where and how coverage changed

File	Statements	Missing	Coverage	Coverage (new stmts)	Lines missing
procrastinate
app.py
cli.py
worker.py
Project Total

This report was generated by python-coverage-comment-action

[onlyann]

Two things I was wondering:

• Should the existing polling option continue to be polling_interval or should it be renamed to something like fetch_polling_interval?

• What should be the default for abort_polling_interval ?
  I kept it to the same default of 5 seconds.

[medihack]

Two things I was wondering:

• Should the existing polling option continue to be polling_interval or should it be renamed to something like fetch_polling_interval?
• What should be the default for abort_polling_interval ?
  I kept it to the same default of 5 seconds.

Yes, in my opinion it would make sense to rename the polling_interval to make things more clear (even to fetch_job_polling_interval).

[ewjoachim]

perfect.

🎉