-
intrigeri authored
Note that this was less mechanical than expected: there are places where "boot menu" means "whatever menu the BIOS/firmware offers to pick a boot device". I did not change those, so now we have two different phrasings, for two different menus, which sounds better than reusing the same wording in both cases.
0d57f78a