/* Flush kernel TLB entries in the given range  */
void flush_tlb_kernel_range(unsigned long start, unsigned long end)
/* Flush kernel TLB entries in the given range  */
void flush_tlb_kernel_range(unsigned long start, unsigned long end)
{
	flush_range(&init_mm, start, end);
	FINISH_FLUSH;
}