/* $Id: testlib.c,v 1.2 2003/06/27 18:24:01 jmmv Exp $ */

#include <stdio.h>

void print_num(int i);

void
print_num(int i)
{
	printf("print_num: %d\n", i);
}