Fix one more broken code include in docs. See #3374