We should do that only after https://github.com/lampepfl/dotty/pull/9476 is merged, since it renames the flag.