[bug-gawk] --lint option and standard input/ouput/error

[M]

When using --lint option, gawk always recommends you to close explicitly any 
file, including special files like standard input, output and error.

However, if a novice follows this piece of advice "as is", he/she will get 
something unexpected. For instance, given the following script (test1.awk):

#########################

BEGIN {
   my_input_resource = "/dev/stdin"

   if ((getline tmp1 < my_input_resource) > 0) {
      print "The first input: " tmp1
   } else {
      print "Error when getting the first input..."
   }

   close(my_input_resource) # Novice: "--lint recommends me to do it..."

   if ((getline tmp2 < my_input_resource) > 0) {
      print "The second input: " tmp2
   } else {
      print "Error when getting the second input..."
   }

   close(my_input_resource)  # Novice: "--lint recommends me to do it..."

   exit
}


#########################

we have (here the line "Print it!" is typed by a user):

$ /path/to/gawk --exec test1.awk
Print it!
The first input: Print it!
Error when getting the second input...
$

Compare with an ordinary file "test.txt" in the following script (test2.awk):

#########################

BEGIN {
   my_input_resource = "test.txt"

   if ((getline tmp1 < my_input_resource) > 0) {
      print "The first input: " tmp1
   } else {
      print "Error when getting the first input..."
   }

   close(my_input_resource)

   if ((getline tmp2 < my_input_resource) > 0) {
      print "The second input: " tmp2
   } else {
      print "Error when getting the second input..."
   }

   close(my_input_resource)

   exit
}

#########################

When running:

$ cat test.txt
Print it!
$ /path/to/gawk --exec test2.awk
The first input: Print it!
The second input: Print it!
$

I don't know whether it's a bug or a feature, but it's quite strange to get 
such pieces of advice with --lint :-).
_______________

Yours respectfully,
Mark Krauze