Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Merge branch 'master' into 'master' master next
authorAugustin Degomme <adegomme@gmail.com>
Sun, 21 Jul 2019 20:11:22 +0000 (22:11 +0200)
committerAugustin Degomme <adegomme@gmail.com>
Sun, 21 Jul 2019 20:11:22 +0000 (22:11 +0200)
MC: complete workaround in the error msg seen on modern systems

See merge request simgrid/simgrid!13


Trivial merge