Merge master branch into dejagnu-1.6.