Reid Kleckner 5fe3f00ae2 Replace wrongly deleted header banner, fix formatting ...

I reviewed the diff hunks of 05da2fe521 that don't contain
'#include' lines, and found two unintended changes. I deleted a header
banner inadvertently while inserting a header, and changed the
indentation of a constructor in an odd way. Add back the banner, and
reformat the constructor.

2019-11-14 10:21:42 -08:00

3.5 KiB

Raw Blame History

View Raw