diff options
| author | JPR | 2019-05-21 23:07:55 +0200 |
|---|---|---|
| committer | JPR | 2019-05-21 23:07:55 +0200 |
| commit | e6322e23958a937fa01960f8ce320717b9863253 (patch) | |
| tree | 79e2a8c8e7c953c44b3880fa683d82f2a6e6cc85 /dev/doc/MERGING.md | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Fixing typos - Part 1
Diffstat (limited to 'dev/doc/MERGING.md')
| -rw-r--r-- | dev/doc/MERGING.md | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md index c9eceb1270..66f5a96802 100644 --- a/dev/doc/MERGING.md +++ b/dev/doc/MERGING.md @@ -92,7 +92,7 @@ When fixes are ready, there are two cases to consider: Once all reviewers approved the PR, the assignee is expected to check that CI completed without relevant failures, and that the PR comes with appropriate documentation and test cases. If not, they should leave a comment on the PR and -put the approriate label. Otherwise, they are expected to merge the PR using the +put the appropriate label. Otherwise, they are expected to merge the PR using the [merge script](../tools/merge-pr.sh). When CI has a few failures which look spurious, restarting the corresponding |