Commit 01a5d326bb320b1e1c832d6954df583ae8c0ebd2

Werner Lemberg 2018-09-04T08:00:58

Make `/****...' comments in public headers uniformly end on column 77.