Merge pull request #1787 from jeromerobert/develop
authorMartin Kroeker <martin@ruby.chemie.uni-freiburg.de>
Thu, 4 Oct 2018 16:41:47 +0000 (18:41 +0200)
committerGitHub <noreply@github.com>
Thu, 4 Oct 2018 16:41:47 +0000 (18:41 +0200)
Fix unknown type name __WAIT_STATUS on RHEL5


Trivial merge