[PATCH 2/5] console-client: entitle console_exit with the noreturn attribute

[Justus Winter <4winter@informatik.uni-hamburg.de>]

* console-client/input.h (console_exit): Add noreturn attribute.
---
 console-client/input.h |    2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/console-client/input.h b/console-client/input.h
index 351fa34..61deadc 100644
--- a/console-client/input.h
+++ b/console-client/input.h
@@ -66,7 +66,7 @@ error_t console_switch (int id, int delta);
 void console_error (const wchar_t *const err_msg);
 
 /* Exit the console client.  Does not return.  */
-void console_exit (void);
+void console_exit (void) __attribute__ ((noreturn));
 
 /* Switch away from the console an external use of the console like
    XFree.  */
-- 
1.7.10.4