1.1 --- a/extras/mini-os/include/ia64/os.h	Thu Jan 17 14:39:21 2008 +0000
     1.2 +++ b/extras/mini-os/include/ia64/os.h	Thu Jan 17 14:39:45 2008 +0000
     1.3 @@ -44,7 +44,7 @@ typedef uint64_t caddr_t;		/* rr7/kernel
     1.4  #include "mm.h"
     1.5  
     1.6  
     1.7 -void do_exit(void);
     1.8 +void do_exit(void) __attribute__((noreturn));
     1.9  void arch_init(start_info_t *si);	/* in common.c */
    1.10  void arch_print_info(void);		/* in common.c */
    1.11  

     2.1 --- a/extras/mini-os/include/x86/os.h	Thu Jan 17 14:39:21 2008 +0000
     2.2 +++ b/extras/mini-os/include/x86/os.h	Thu Jan 17 14:39:45 2008 +0000
     2.3 @@ -21,7 +21,7 @@
     2.4  
     2.5  #define USED    __attribute__ ((used))
     2.6  
     2.7 -extern void do_exit(void);
     2.8 +extern void do_exit(void) __attribute__((noreturn));
     2.9  #define BUG do_exit
    2.10  
    2.11  #endif