You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Good idea.
Currently, CI does not actually run the analysis. What is costly is to download all the issues of Agda (which the py script currently does). This is very slow because of GitHub API throttling. I could check in the JSON file with the issues after downloading though, and this could be updated time after time.
Last time I looked, while one can upload arbitrary files with this action, one can only download these as ZIP files. It would be nicer to publish the PNGs directly.
So maybe instead of CI, I could also check in the PNGs with the JSON file, together with a HTML file that embeds them...
So maybe instead of CI, I could also check in the PNGs with the JSON file, together with a HTML file that embeds them...
Wow, that would be even better. The agda-stdlib trick may also be useful, as you can commit the png to a particular branch (in which you can delete from time to time to reduce repo size) and refer to it as an imagefile.
As title. You may use https://github.com/actions/upload-artifact
The text was updated successfully, but these errors were encountered: