is the bot dead

Stream: triage

[Johan Commelin]

The bot seems dead...

[Bryan Gin-ge Chen]

It seems to be sleeping because we haven't touched the repo in a while: https://github.com/leanprover-community/azure-scripts/actions/workflows/random_issue.yml

BTW did we want to switch to mathlib4 issues / PRs? https://github.com/leanprover-community/azure-scripts/pull/14

[Bryan Gin-ge Chen]

I've gone ahead and re-enabled all the workflows in the repo. However, it seems that the "Delete old archives from Azure" job has been failing for a while:

https://github.com/leanprover-community/azure-scripts/actions/runs/6031893893

Maybe we changed an API key without updating the secret?

[Bryan Gin-ge Chen]

@Scott Morrison Sorry! I realized the bot still wasn't fully updated, so I made some more fixes: https://github.com/leanprover-community/azure-scripts/pull/16 :pray: