26f28ea Fix type of printf argument

1 file Authored by sbose 10 years ago, Committed by mkosek 10 years ago,
    Fix type of printf argument