Merge branch 'good_hist' into gmaster

A force push to master rewrote history and dropped these commits.
We need to add them back.