first attempt #16557
jcommelin
merged
9 commits into
leanprover-community:master
from
jcommelin:maintainer-merge-jmc
first attempt
97b0505d
add bot
8b0bedfc
throw away useless steps
8d4e056b
shorter name
436110bd
format message
921a0472
add rocket emoji to maintainer merge comment
0d6f79ef
also run workflow on reviews
7e7dc6bb
longer if clause to include review comments
508cd915
for testing purposes only
b1159065
Reviewers
No reviews
Assignees
No one assigned
Labels
None yet
Milestone
No milestone
Login to write a write a comment.
Login via GitHub