GRUB maintainer, Hey, quick bug – on the html documentation index (http://www.gnu.org/software/grub/manual/grub/html_node/index.html), it lists the title of section 16.3.21 as “linux" instead of “devicetree”. This is replicated in the heading on the referenced html page, but shows the correct devicetree command and description.
Hope that helps! Justin Kearse
