/* porttime.c -- portable API for millisecond timer */
/* There is no machine-independent implementation code to put here */