Revert "remove pasted comment"

This reverts commit c33c49295d.
2023-11-19 17:36:00 -05:00
parent 2cbbfbe648
commit a42d3dadce
1 changed files with 1 additions and 0 deletions
@@ -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: