531,533d530
<     if { $log != "stdout" } {
<       close $log
<     }