Subject: Re: bug#67391: dejagnu report card and multiple rows

From: Jacob Bachmeyer <[email-masked]>
Date: Tue, 12 Dec 2023 20:40:20 -0600

The documentation patch on the PR67391 branch has been merged to master, 
explaining the totals line at the end of "dejagnu report card" output.  
Closing issue.

-- Jacob