public int get_height_mm ()
Warning: get_height_mm is deprecated since 3.22.
Returns the height of this in millimeters.
Use per-monitor information instead
Note that this value is somewhat ill-defined when the screen has multiple monitors of different resolution. It is recommended to use the monitor dimensions instead.
the heigth of this in millimeters.