Topic: Travis okays sorry
Chris Hughes (Aug 26 2019 at 14:53):
Travis is has #1297 down as a build success, even though there are sorries. Perhaps this behaviour should be changed.
Johan Commelin (Aug 26 2019 at 14:54):
I must agree with Travis that #1297 is a big success (-;
Last updated: May 11 2021 at 16:22 UTC