/* Free a block created with ipc_alloc(). The caller must know the size used in the allocation call.  */
void ipc_free(void *ptr, int size)
/* Free a block created with ipc_alloc(). The caller must know the size used in the allocation call.  */
void ipc_free(void *ptr, int size)
{
	if(size > PAGE_SIZE)
		vfree(ptr);
	else
		kfree(ptr);
}