Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Add mathlib4 porting comments #427

Add mathlib4 porting comments

Add mathlib4 porting comments #427

Triggered via schedule December 6, 2023 00:20
Status Success
Total duration 47s
Artifacts

add_port_comment.yml

on: schedule
Update comments
38s
Update comments
Fit to window
Zoom out
Zoom in

Annotations

1 warning
Update comments
The following actions uses node12 which is deprecated and will be forced to run on node16: actions/github-script@v5. For more info: https://github.blog/changelog/2023-06-13-github-actions-all-actions-will-run-on-node16-instead-of-node12-by-default/