diff options
| author | Théo Zimmermann | 2018-12-23 18:05:18 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-23 19:45:23 +0100 |
| commit | 1e9ccebec7478ded30b8ace96e4ddab8b14b410f (patch) | |
| tree | 1e85e363892ca816438955c0df93217e5aa72045 /dev/ci | |
| parent | b878216ca5e85f8164fa098b9dc0e688a212072d (diff) | |
[ci] Annotate plugins and libraries.
This will allow @coqbot to automatically add appropriate needs labels
(overlay or fixing) depending on whether it breaks a plugin or a library.
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions