TIMESTAMP = 1603072890
SHA256 (MUMPS_4.10.0.tar.gz) = d0f86f91a74c51a17a2ff1be9c9cee2338976f13a6d00896ba5b43a5ca05d933
SIZE (MUMPS_4.10.0.tar.gz) = 2481516
SHA256 (coin-or-tools-ThirdParty-Mumps-releases-1.6.2_GH0.tar.gz) = 0cfdd30b9cb42d9539ad9c495629f56dd1fc0b59cea691bbe71a129fabd8895d
SIZE (coin-or-tools-ThirdParty-Mumps-releases-1.6.2_GH0.tar.gz) = 269074