fix broken compilation

Authored by cgilles on May 25 2020, 1:52 AM.