1 files changed, 2 insertions, 0 deletions

diff --git a/lib-src/make-docfile.c b/lib-src/make-docfile.c
index ccd245e0139..4d25b0a6b93 100644
--- a/lib-src/make-docfile.c
+++ b/lib-src/make-docfile.c
@@ -747,6 +747,8 @@ write_globals (void)
             printf ("%d", globals[i].v.value);
           putchar (')');
 
+          if (globals[i].flags & DEFUN_noreturn)
+            fputs (" ATTRIBUTE_COLD", stdout);
           if (globals[i].flags & DEFUN_const)
             fputs (" ATTRIBUTE_CONST", stdout);