diff options
| author | Emilio Jesus Gallego Arias | 2019-01-23 13:46:52 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-01-23 13:46:52 +0100 |
| commit | 398b13bb6937cca90c685e4f8dba6a1db60a103e (patch) | |
| tree | 6040ad18c73c7742ee71e111b20cd4bedf7cffb5 | |
| parent | 163000a8326ad559d2a0581608f2ccc83fe3beee (diff) | |
| parent | 9aad49b0655404055c4f0aa96d203a5e6cdcf07e (diff) | |
Merge PR #9339: Move plugin tutorial to team ownership
Reviewed-by: ejgallego
Reviewed-by: gares
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index ecfeac65ad..275d6c1ff5 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -70,7 +70,7 @@ azure-pipelines.yml @coq/ci-maintainers /man/ @silene # Secondary maintainer @maximedenes -/doc/plugin_tutorial/ @ybertot +/doc/plugin_tutorial/ @coq/plugin-tutorial-maintainers ########## Coqchk ########## |