+ /*
+ * Even if HDMI0 on the RPi4 can output modes requiring a pixel
+ * rate higher than 297MHz, it needs some adjustments in the
+ * config.txt file to be able to do so and thus won't always be
+ * available.
+ */
+ bool vc5_hdmi_enable_hdmi_20;
+
+ /*
+ * 4096x2160@60 requires a core overclock to work, so register
+ * whether that is sufficient.
+ */
+ bool vc5_hdmi_enable_4096by2160;