diff --git a/src/system/kernel/platform/pxe_ia32/platform.cpp b/src/system/kernel/platform/pxe_ia32/platform.cpp new file mode 100644 index 0000000000..c30c0cc959 --- /dev/null +++ b/src/system/kernel/platform/pxe_ia32/platform.cpp @@ -0,0 +1,3 @@ +/* + Just a dummy. No BIOS services are required in the kernel. +*/