/* porttime.c -- portable API for millisecond timer */

/* There is no machine-independent implementation code to put here */