/*- * This file is in the public domain. */ #include <x86/xen/xen-os.h>