diff options
| -rw-r--r-- | debian/patches/70_dde.patch | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/debian/patches/70_dde.patch b/debian/patches/70_dde.patch index a91abf2..6d488c3 100644 --- a/debian/patches/70_dde.patch +++ b/debian/patches/70_dde.patch @@ -742,17 +742,15 @@ console_map_init(); --- a/kern/ipc_kobject.c +++ b/kern/ipc_kobject.c -@@ -152,7 +152,8 @@ ipc_kobject_server(request) - device_server_routine(), - device_pager_server_routine(), - mach4_server_routine(), -- gnumach_server_routine(); -+ gnumach_server_routine(), -+ experimental_server_routine(); - #if MACH_DEBUG - extern mig_routine_t mach_debug_server_routine(); - #endif -@@ -172,6 +173,7 @@ ipc_kobject_server(request) +@@ -56,6 +56,7 @@ + #include <device/device_pager.server.h> + #include <kern/mach4.server.h> + #include <kern/gnumach.server.h> ++#include <kern/experimental.server.h> + + #if MACH_DEBUG + #include <kern/mach_debug.server.h> +@@ -173,6 +174,7 @@ ipc_kobject_server(request) #endif /* MACH_DEBUG */ || (routine = mach4_server_routine(&request->ikm_header)) != 0 || (routine = gnumach_server_routine(&request->ikm_header)) != 0 |