Merge from CEDET upstream (8564).