[SV 33134] Don't try to close stdout when it's already closed.

1 files changed, 0 insertions, 2 deletions

diff --git a/makeint.h b/makeint.h
index 276a13d9..dac58587 100644
--- a/makeint.h
+++ b/makeint.h
@@ -493,8 +493,6 @@ void user_access (void);
 void make_access (void);
 void child_access (void);
 
-void close_stdout (void);
-
 char *strip_whitespace (const char **begpp, const char **endpp);
 
 /* String caching  */