*** empty log message ***

[splint.git] / src / llmain.c

diff --git a/src/llmain.c b/src/llmain.c
index 8210121cec889f477047686166d4ed77ce6e0f8e..82922fa8b53fc2130cdee1e76dedcc7b9632a575 100644 (file)
--- a/src/llmain.c
+++ b/src/llmain.c
@@ -94,7 +94,7 @@ static void showHelp (void);
 static void interrupt (int p_i);
 
 static void loadrc (/*@open@*/ FILE *p_rcfile, cstringSList *p_passThroughArgs)
-     ; // /*@ensures closed p_rcfile@*/ ;
+     /*@ensures closed p_rcfile@*/ ;
 
 static void describeVars (void);
 static bool specialFlagsHelp (char *p_next);
@@ -2146,7 +2146,7 @@ llexit (int status)
 
 void
 loadrc (/*@open@*/ FILE *rcfile, cstringSList *passThroughArgs)
-     //    /*@ensures closed rcfile@*/
+   /*@ensures closed rcfile@*/
 {
   char *s = mstring_create (MAX_LINE_LENGTH);
   char *os = s;