I tried the old "close it and re-open" trick which didn't seem to help.
Then I checked https://www.githubstatus.com/ and sure enough it says
"GitHub Actions is experiencing degraded performance. We are still
investigating and will provide an update when we have one. Feb 5, 22:25
UTC". This is almost surely why we aren't seeing the checks run.
On 2/5/22 15:23, Glauco wrote:
Here
https://github.com/metamath/set.mm/pull/2473
no check have been performed.
Is this a known issue? (there is no recent open issue on github)
Glauco
--
You received this message because you are subscribed to the Google
Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send
an email to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/51b0df83-9169-4f48-964f-7cbeeef75f80n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/51b0df83-9169-4f48-964f-7cbeeef75f80n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0ac64dec-ef1d-7643-80f3-0c44d4ad92ac%40panix.com.
