Rémi Verschelde b30014f93f DocData: Keep Mono properties on non-Mono builds
This doesn't make much sense API-wise, but it's important for the documentation
workflow that the Mono and non-Mono builds produce the same output, otherwise
we keep having non-Mono builds removing Mono properties and losing their
descriptions.

This is a terrible hack but it's ad hoc, and should be OK for the time being.
2020-04-20 17:59:07 +02:00
..
2020-01-01 11:16:22 +01:00
2020-04-02 13:38:00 +02:00