Pull request done! On a sidenote: the instructions at Libreboot for making pull requests,
https://libreboot.org/git.html#how-to-submit-your-patches-via-pull-requestsare VERY useful. I recently heard that a large part of people starting to work in software development have never heard of pull-requests, and would wonder why they can't just push to master directly. Not only is Libreboot good for free bios replacements, but also for teaching good habits in coding!
