Eric Christopher <echristo@redhat.com> writes: > The patch is already in the mainstream dejagnu sources I'm waiting > on bje to bring it into sources.redhat.com. You can commit the patch to src/dejagnu if it's really important, however I would like to see src/deajgnu go away altogether. Ben