5 commits

Author	SHA1	Message	Date
JAremko	7c7843d121	[ci] fix patching	2021-07-07 05:40:23 -07:00
JAremko	d78d8282f5	[ci] Handle the case when everything is up to date	2021-07-05 16:47:38 -07:00
JAremko	88cfc4bc67	[ci] fix ws in patches and use git apply	2021-07-05 15:47:43 -07:00
JAremko	6f8d6d5b3a	[ci] Don't mask push outputs (CircleCI masks secrets anyway)	2021-07-05 15:09:53 -07:00
JAremko	aa4547086d	[CI] Move documentation formatting to CircleCI	2021-07-05 14:30:55 -07:00