Warning to python coders:

int()

is equivalent to

trunc()

not

round()

. Found a case in the

gen_gpio_defaults.py

script where

1914.9999999999998

becomes

1914

instead of the expected

1915

.