pocmatos
2020-4-25 09:57:09

@sorawee I contacted github engs. about the internal error issue. Waiting to hear something.


pocmatos
2020-4-25 09:58:14

I don’t know if we can allow PR-ers to restart CI. Danger to GitHub is a lot more heavy load on their servers… however! You can commit an empty change to your PR. That should do it. You can call it ‘Force CI’. Then when squashing / merging, that detail is removed.


sorawee
2020-4-25 10:30:45

Well, I mean, I don’t think “a lot more heavy load on their servers” makes sense here, since committing empty change can also make the heavy load as well.


pocmatos
2020-4-25 10:32:26

I thought that could be a reason for them not to add the functionality to do that… I didn’t mean there couldn’t be a workaround. The workaround is to just push an empty commit. :slightly_smiling_face:


sorawee
2020-4-25 11:21:21

Makes sense


pocmatos
2020-4-25 13:55:51

… that’s just me guessing btw - I have no real information about this.