Robin Gloster af9f44dd57 grub: fix capitalisation ... Missed this occurence while renaming the option		2017-02-13 14:55:36 +01:00
..
activation
boot	grub: fix capitalisation	2017-02-13 14:55:36 +01:00
etc