[Tcwg-commits] [dejagnu] branch PR71624 created (now 42979bd)