Rebase rdicosmo PR #1106

(it contained merge commits ; better to rebase than merge on personal branches)