From a42d3dadcef8b073064e422614395ddffb739c9c Mon Sep 17 00:00:00 2001
From: nhmall <nhmall@nethack.org>
Date: Sun, 19 Nov 2023 17:36:00 -0500
Subject: [PATCH] Revert "remove pasted comment"

This reverts commit c33c49295d6da0aeb5e1dfec027f8c7448c29323.
---
 util/makedefs.c | 1 +
 1 file changed, 1 insertion(+)

diff --git a/util/makedefs.c b/util/makedefs.c
index 98a209c5c..7c046491f 100644
--- a/util/makedefs.c
+++ b/util/makedefs.c
@@ -363,6 +363,7 @@ do_makedefs(char *options)
                 " for '%c' (%s) support.\n",
                 *options, oldfunctionality(*options));
             (void) fflush(stderr);
+            /*NOTREACHED*/
             break;
 #endif /* OLD_MAKEDEFS_OPTIONS */
         default: