diff options
| author | Rémi Verschelde <rverschelde@gmail.com> | 2023-01-20 13:10:00 +0100 |
|---|---|---|
| committer | Rémi Verschelde <rverschelde@gmail.com> | 2023-01-20 13:13:38 +0100 |
| commit | f461a005bd601b14c9d1980f9c703d791131b444 (patch) | |
| tree | 05a6ae56adfec671de5b4498ad6c225aaccda37d /misc/ci | |
| parent | 621e32971edc27bd1c2f3528534423a5a805d8e7 (diff) | |
doc: Define dummy Mono settings to keep them in doctool
Revival of #54840.
Diffstat (limited to 'misc/ci')
0 files changed, 0 insertions, 0 deletions