diff options
author | Rémi Verschelde <rverschelde@gmail.com> | 2023-01-20 17:52:03 +0100 |
---|---|---|
committer | Rémi Verschelde <rverschelde@gmail.com> | 2023-01-20 17:52:03 +0100 |
commit | fe17e6d2f230de5a91b61d784d80c193473698e3 (patch) | |
tree | 283fc8b235eb0e5e40616bb2298b0650d0bf7acf /editor/editor_folding.h | |
parent | 42d3e62455058bc4d7f45af6877812ea387b527a (diff) | |
parent | f461a005bd601b14c9d1980f9c703d791131b444 (diff) |
Merge pull request #71728 from akien-mga/doc-preserve-mono-settings
doc: Define dummy Mono settings to keep them in doctool
Diffstat (limited to 'editor/editor_folding.h')
0 files changed, 0 insertions, 0 deletions