Didn't we use to have direct links to logs on gitlab instead of going through the github checks page?
ie https://gitlab.com/coq/coq/-/jobs/3034676107 instead of https://github.com/coq/coq/pull/16493/checks?check_run_id=8379143914
Hum, that was a very long time ago (before coqbot started to use the Checks tab in 2020), wasn't it?
Adding direct links without removing the Checks feature would unfortunately amount to duplicating every failed check.
Théo Zimmermann said:
Hum, that was a very long time ago (before coqbot started to use the Checks tab in 2020), wasn't it?
after using the checks tab the direct links were made to work again until recently
or maybe it's an extension I had that stopped working? not sure
or maybe it's an extension I had that stopped working? not sure
Probably, because I don't recall anything like this.
I am using the refined github extension which makes the links direct. Occasionally it stops working and takes me to the checks tabs.
Last updated: May 28 2023 at 18:29 UTC