diff options
| author | Gaëtan Gilbert | 2019-01-11 13:59:55 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:42:11 +0100 |
| commit | 9aad49b0655404055c4f0aa96d203a5e6cdcf07e (patch) | |
| tree | 2540fee74944689b3b935f04edf57d603f45de1e | |
| parent | ac8c25a9fac51745f0b53162fba48ef5b86d227d (diff) | |
Move plugin tutorial to team ownership
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 2a641263e3..54d9ccaf19 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -71,7 +71,7 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes -/doc/plugin_tutorial/ @ybertot +/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers ########## Coqchk ########## |