extended CI does not reliably trigger when auto-merge is on

[BenWibking]

With the past few PR's I've merged (related to sanitizer warnings), the extended CI didn't trigger when I had auto-merge enabled. In all cases, I had to turn off auto-merge, then turn it back on. Then the extended CI triggered automatically.

Is it known why this is the case? It is just GitHub being flaky?

[lroberts36]

Yeah, I have similar problems often (and often try the same trick as you did) but I don't know why this happens.

[pgrete]

IIRC the extended test are not triggered by changes made through the Github UI (like merging in develop or applying formatting).

[BenWibking]

IIRC the extended test are not triggered by changes made through the Github UI (like merging in develop or applying formatting).

ah, that would explain some things...