Commit 323dabef4b3570798e2d9daedbba9b98e9d7a504

Paul Eggert 2016-03-31T16:40:20

Merge branch 'micro' into minor