Summary of changes: 921e069... 4.7.2 (*) ded6d74... drop old stuff (*) d72d8fa... Release: 1 drop an old (unuseful) patch that no longer appl (*) (*) This commit already existed in another branch; no separate mail sent