9ed8fd9 Fix documentation build failure

Authored and Committed by walki 2 years ago
    Fix documentation build failure
    
        
file modified
+4 -9