1 /* 2 * (c) 2008-2009 Adam Lackorzynski <adam@os.inf.tu-dresden.de> 3 * economic rights: Technische Universität Dresden (Germany) 4 * 5 * This file is part of TUD:OS and distributed under the terms of the 6 * GNU General Public License 2. 7 * Please see the COPYING-GPL-2 file for details. 8 */ 9 #ifndef INIT_H 10 #define INIT_H 11 12 #include <l4/sys/compiler.h> 13 14 #define INIT_SECTION __attribute__((section (".init"))) 15 16 #ifdef __cplusplus 17 extern "C" 18 #endif 19 void init(l4_kernel_info_t *info) L4_NORETURN; 20 21 #endif 22