Subject: Re: bug#67391: dejagnu report card and multiple rows
From: Jacob Bachmeyer <[email-masked]>
To: Tom Tromey <[email-masked]>
Cc: [email-masked]
Date: Tue, 12 Dec 2023 20:40:20 -0600
List-Id: <debbugs-submit.debbugs.gnu.org>

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