Add missing commit from PR 354

This patch adds a commit that was missing from the merge of PR 354,
commit ef7c3adccd3c13d358c97479d14094d7574d6abb.