Fix warning that was printed spuriously. #75

Closed floitsch closed 1 year ago