diff options
| author | Théo Zimmermann | 2018-11-06 16:14:21 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-11-22 13:57:48 +0100 |
| commit | 29adf6d7d040a1721e63e1ad02bb1c3e8847ff8c (patch) | |
| tree | 24a06384aafa438f07176aca334c2929c7f3baeb | |
| parent | 31d0ba99849b96914379aaf4f79a81c0142bc211 (diff) | |
It seems that Hugo is also willing to assume a maintainer role on CoqIDE.
| -rw-r--r-- | .github/CODEOWNERS | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 13e6029255..802c1da221 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -105,7 +105,7 @@ /ide/ @ppedrot /test-suite/ide/ @ppedrot -# Secondary maintainer @gares +# Secondary maintainers @gares @herbelin ########## Interpretation ########## |