diff options
| author | Emilio Jesus Gallego Arias | 2019-03-21 02:07:17 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-21 02:07:17 +0100 |
| commit | 4a547c6aa58ef902c0a883d4be77761537a86280 (patch) | |
| tree | 61c848238d70291162972a62a7878923810f486d /dev/ci | |
| parent | d3f40cad021e3c794be99cb90f0e2869ab389f40 (diff) | |
| parent | 0063c4c985078fd181c4a3a149ccbb06752edc97 (diff) | |
Merge PR #9774: Remove clutter by moving historic unmaintained dev/doc files to an archive subfolder.
Reviewed-by: ejgallego
Diffstat (limited to 'dev/ci')
0 files changed, 0 insertions, 0 deletions