Merge pull request #4089
74fc254 devtools: add script to check symbols from Linux gitian executables (Wladimir J. van der Laan)