Closed fchapoton closed 1 year ago
should I add an entry in the news ?
should I add an entry in the news ?
I added something.
@fchapoton thanks for the PR. I adapted the workflow to what we're using for e-antic so we don't have to maintain two different workflows. I also fixed some more typos/grammar.
Checklist
doc/news/
.