>>>> + 8042 at 60 {
>>>> + device_type = "8042";
>
>> Drop the device_type. A number as a name isn't
>> all that great, either.
>
> Yet it's kinda accepted years ago, see:
>
> http://playground.sun.com/1275/proposals/Closed/Accepted/381-it.txt
That's not a published recommendation or anything like that.
Segher