Revision 8e913baeeeb9f00f8ecce593b42eb79da6481884

Committed on 15/03/2012 8:42 am by Nicolas Pastorino <nfrp@ez.no> [GitHub Diff]

Reverted pull-request #9 now that the underlying causes of #19107 were
fixed.