*/
/* IPC initialization needed before creation of kernel task */
-extern void ipc_bootstrap(void) __attribute__((section("__TEXT, initcode")));
+extern void ipc_bootstrap(void);
/* Remaining IPC initialization */
-extern void ipc_init(void) __attribute__((section("__TEXT, initcode")));
+extern void ipc_init(void);
#endif /* _IPC_IPC_INIT_H_ */