Files
infix/.github
Joachim Wiberg 6583b1e451 .github: simplify Bob's workflow and don't move latest tag [skip ci]
We only want Bob to run when PR's have been merged to main, this means
when something is pushed to main.  (Took a while to figure this one out
actually.)  See the following community discussion for details:

https://github.com/orgs/community/discussions/26724#discussioncomment-3253102

Also, we've seen that moving the 'latest' tag messes up any push/pull/sync
operation between clones and forks, so let's skip it and see how that works.

Signed-off-by: Joachim Wiberg <troglobit@gmail.com>
2023-10-03 13:39:56 +02:00
..