difftime.c

#ifndef lint
#ifndef NOID
static char	elsieid[] = "%W%";
#endif /* !defined NOID */
#endif /* !defined lint */

/*LINTLIBRARY*/

#include "private.h"

double
difftime(time1, time0)
const time_t	time1;
const time_t	time0;
{
	return time1 - time0;
}
created 1989-02-24 18:51:47 -05:00			`#ifndef lint`
			`#ifndef NOID`
			`static char elsieid[] = "%W%";`
			`#endif /* !defined NOID */`
			`#endif /* !defined lint */`

			`/LINTLIBRARY/`

headers redone; delinted 1989-03-21 11:37:19 -05:00			`#include "private.h"`
created 1989-02-24 18:51:47 -05:00
			`double`
			`difftime(time1, time0)`
			`const time_t time1;`
			`const time_t time0;`
			`{`
			`return time1 - time0;`
			`}`