You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
So long as we have a GitHub based publication process, there some messages we will want to post directly on PRs. This topic has come up in several places, most recently in #372
Even once we have need to mature beyond that basis, having a bot associated with opam.ci is likely to be useful. Moreover, we can use the opam-bot account to automate interactions with GitHub, which would help support adding a customized review/publication layer as an alternative (or augment) to the GitHub web UI (should that be desirable).
The text was updated successfully, but these errors were encountered:
So long as we have a GitHub based publication process, there some messages we will want to post directly on PRs. This topic has come up in several places, most recently in #372
Even once we have need to mature beyond that basis, having a bot associated with opam.ci is likely to be useful. Moreover, we can use the opam-bot account to automate interactions with GitHub, which would help support adding a customized review/publication layer as an alternative (or augment) to the GitHub web UI (should that be desirable).
The text was updated successfully, but these errors were encountered: