[devdocsgjs/main: 1383/1867] docs/maintainers: update "Merging pull requests"
- From: Andy Holmes <andyholmes src gnome org>
- To: commits-list gnome org
- Cc:
- Subject: [devdocsgjs/main: 1383/1867] docs/maintainers: update "Merging pull requests"
- Date: Fri, 19 Nov 2021 23:47:56 +0000 (UTC)
commit 88c44a72ce25c18422e2a30a16fc3bc668b796c7
Author: Simon Legner <Simon Legner gmail com>
Date: Wed Nov 25 09:24:03 2020 +0100
docs/maintainers: update "Merging pull requests"
docs/maintainers.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
---
diff --git a/docs/maintainers.md b/docs/maintainers.md
index 1cc72e94..1366543d 100644
--- a/docs/maintainers.md
+++ b/docs/maintainers.md
@@ -6,7 +6,7 @@ This document is intended for [DevDocs maintainers](#list-of-maintainers).
- PRs should be approved by at least one maintainer before being merged.
-- PRs that add or update documentations should always be merged locally, and the app deployed, before the
merge is pushed to GitHub.
+- PRs that add or update documentations should always be built and tested locally, and the doc files
uploaded by the `thor docs:upload` command, before the PR is merged on GitHub.
This workflow is required because there is a dependency between the local and production environments. The
`thor docs:download` command downloads documentations from production files uploaded by the `thor
docs:upload` command. If a PR adding a new documentation is merged and pushed to GitHub before the files have
been uploaded to production, the `thor docs:download` will fail for the new documentation and the docker
container will not build properly until the new documentation is deployed to production.
[
Date Prev][
Date Next] [
Thread Prev][
Thread Next]
[
Thread Index]
[
Date Index]
[
Author Index]