diff options
Diffstat (limited to 'boot')
| -rw-r--r-- | boot/Makefile | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/boot/Makefile b/boot/Makefile index e57159ef..9b23c7f1 100644 --- a/boot/Makefile +++ b/boot/Makefile @@ -50,7 +50,10 @@ exec_S.h execServer.c: $(headers)/hurd/exec.defs $(MIGCOM) -user /dev/null -header /dev/null \ -sheader exec_S.h -device_S.h deviceServer.c: $(headers)/device/device.defs +device.defs: $(headers)/device/device.defs + sed -e '/out device : device_t/s/device_t/mach_port_send_t/' $< > $@ + +device_S.h deviceServer.c: device.defs $(CPP) $(CPPFLAGS) $< | \ $(MIGCOM) -user /dev/null -header /dev/null \ -sheader device_S.h |