mpfrlint: update for git.
This is used to check that the doc/mpfr.texi UPDATED-MONTH value is up-to-date by comparing it with the date of the latest commit.
Si vous êtes un personnel Inria et que vous souhaitez participer aux tests de notre future plateforme Gitlab basée sur la version ultimate avec gitlab LFS activé merci de contacter Didier Chassignol.
This is used to check that the doc/mpfr.texi UPDATED-MONTH value is up-to-date by comparing it with the date of the latest commit.
mentioned in commit 136e48c9
·mentioned in commit 136e48c9
mentioned in commit c049c97e
·mentioned in commit c049c97e