Just for the record: There was something odd going on with the coverity-scan branch (which pointed to the same commit as this PR) and Travis CI, such that this PR run the coverity-scan branch script, which failed. I made another branch and PR (pointing to this commit), and it worked. Don't ask me what was happening here, it did not feel so important to investigate it further.
Just for the record: There was something odd going on with the coverity-scan branch (which pointed to the same commit as this PR) and Travis CI, such that this PR run the coverity-scan branch script, which failed. I made another branch and PR (pointing to this commit), and it worked. Don't ask me what was happening here, it did not feel so important to investigate it further.