/* (RJJ) some programs look for the DDK header here...  */

#include <ddk/ntddk.h>