diff options
author | Justus Winter <4winter@informatik.uni-hamburg.de> | 2013-10-10 18:08:19 +0200 |
---|---|---|
committer | Samuel Thibault <samuel.thibault@ens-lyon.org> | 2013-10-13 17:56:15 +0200 |
commit | 9be362ab7efc6ad27a678e00f9b0b35a24993aa1 (patch) | |
tree | 782e75d1a7d275ca7f0f2d0eb44a94a076b522d9 | |
parent | 695e5d209ade018afea1b2d2f9e042e9c78028ae (diff) |
console-client: entitle console_exit with the noreturn attribute
* console-client/input.h (console_exit): Add noreturn attribute.
-rw-r--r-- | console-client/input.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/console-client/input.h b/console-client/input.h index 351fa34a..61deadc0 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. */ |