Open Dacit opened 3 months ago
I definitely think it should be ok to PR many results at once, especially at the start. Restricting to 1 ITP seems good though.
I also don't mind multiple thm PRs, but agree that it would be good if they're just for a single system, mostly because I would like the person responsible for the system to be the one to decide about it (more specifically: about what convention to use for links and identifiers), but then also to be the one that accepts the PR.
We should give guidelines on how the PRs should look like -- I would suggest that they only touch a single thm, and should be labelled by which ITP they are for.