This comes with the intentionally undocumented --disable-randr15 command
line flag and disable-randr15 configuration directive. We will add
documentation before the release if and only if it turns out that users
actually need to use this flag in their setups. Ideally, nobody would
need to use the flag and everything would just keep working, but it’s
better to be safe than sorry.
fixes#1799