Xavier Morel 52f2b1e381 [FIX] runbot_merge: don't show details of merged PR on GH ... Detailed statuses are useful in the actual PR dashboard as that allows direct access to the builds, however in the PR where it's only a picture it's useless, so fold that information. Also fold it when a PR is staged. And while at it add a note / sub-title that the PR is staged. Fixes #919		2024-08-05 15:18:19 +02:00
..
__init__.py	[CHG] runbot_merge: log ping instead of printing it	2024-06-25 15:54:31 +02:00
dashboard.py	[FIX] runbot_merge: don't show details of merged PR on GH	2024-08-05 15:18:19 +02:00
reviewer_provisioning.py	[FIX] runbot_merge: make provisioning more resilient	2023-06-21 14:26:19 +02:00