27e117307d
The mpconfigport.h file is an internal header and should only ever be included once by mpconfig.h. Signed-off-by: Damien George <damien@micropython.org>