August hiatus and pull requests

Could we get advice from the chair or editors: during our August hiatus
should pull requests also be partially or wholly curtailed? Put another
way, are there certain GitHub activities types that should be avoided until
the community group has reassembled?

Best wishes,

jk
-- 
Joel Kalvesmaki
kalvesmaki.com

Received on Thursday, 20 July 2023 02:49:01 UTC