Now that we gather on-board devices from both DMI types 10 and 41, there is
a possibility that we list the same device twice.  In order to not confuse
drivers, and also to save memory, make sure that we do not add duplicate
devices to the dmi_devices list.

Signed-off-by: Jean Delvare <khali@linux-fr.org>
Cc: Wim Van Sebroeck <wim@iguana.be>
Signed-off-by: Andrew Morton <akpm@linux-foundation.org>
Signed-off-by: Linus Torvalds <torvalds@linux-foundation.org>