[coreboot] Patch merged into coreboot/master: 8d71155 Rename devices -> device

the following patch was just integrated into master:
commit 8d7115560d469f901d7d8ccb242d0b437e7394aa
Author: Stefan Reinauer 
Date:   Fri Nov 30 12:34:04 2012 -0800

Rename devices -> device

to match src/include/device

Change-Id: I5d0e5b4361c34881a3b81347aac48738cb5b9af0
    Signed-off-by: Stefan Reinauer 
    Reviewed-on: http://review.coreboot.org/1960
    Tested-by: build bot (Jenkins)
    Reviewed-by: David Hendricks

Build-Tested: build bot (Jenkins) at Fri Nov 30 23:35:56 2012, giving +1
Reviewed-By: David Hendricks  at Fri Nov 30 23:38:43 2012, giving +2
See http://review.coreboot.org/1960 for details.

-gerrit