[coreboot-gerrit] Patch merged into coreboot/master: grub: Build module `boottime`

[gerrit at coreboot.org]

the following patch was just integrated into master:
commit 7c7b1761691864158c51d6a99f74e2e4a3e9ca0e
Author: Paul Menzel <pmenzel at molgen.mpg.de>
Date:   Fri Jan 20 17:30:00 2017 +0100

    grub: Build module `boottime`
    
    Configure GRUB to build with boot time statistics. That allows users
    to add that module to GRUB by adding `boottime` to the list of extra
    modules.
    
    Change-Id: I76a07e49aecb37652fe8c7d6a9421fd464424287
    Signed-off-by: Paul Menzel <pmenzel at molgen.mpg.de>
    Reviewed-on: https://review.coreboot.org/18367
    Tested-by: build bot (Jenkins)
    Reviewed-by: Patrick Rudolph <siro at das-labor.org>


See https://review.coreboot.org/18367 for details.

-gerrit