revert 94c0f1, was wrong
Authored by: Jean-Francois Dockes 2017-09-27
Parent(s): [e6cd90]
Child(ren): [90033c]