commit push rule: accept "doc" as commit type (in addition to "docs", the plural may have been confusing).

documentation/dev-guide.md

@@ -214,7 +214,7 @@ Commits are first described by the type of their content, listed in the followin
 | fix      | bug fix                                                                                                                                    |
 | chore    | changes that do not relate to a fix or feature and don't modify src or test files (for example updating dependencies)                      |
 | refactor | refactored code that neither fixes a bug nor adds a feature                                                                                |
-| docs     | updates to documentation such as a the README or other markdown files                                                                      |
+| docs (or "doc")     | updates to documentation such as a the README or other markdown files                                                                      |
 | style    | changes that do not affect the meaning of the code, likely related to code formatting such as white-space, missing semi-colons, and so on. |
 | test     | including new or correcting previous tests                                                                                                 |
 | perf     | performance improvements                                                                                                                   |