mirror of
https://github.com/odoo/runbot.git
synced 2025-03-19 17:35:45 +07:00
![]() If a PR is closed on github and unknown by the mergebot, when fetched it should be properly sync'd as "closed" in the backend, otherwise the PR can get in a weird state and cause issues. Also move the "I fetched the thing" comment before the actual creation of the PR for workflow clarity, otherwise the reader has the impression that the 'bot knew about the PR then fetched it anyway. And improve savepoint management around the fetching: savepoints should be released in all cases. Closes #488. |
||
---|---|---|
.. | ||
__init__.py | ||
pull_requests.py | ||
res_partner.py |