[SeaBIOS] [PATCH 9/9] stdvga: Rename stdvga_get_vde() to stdvga_get_vertical_size()