Merge pull request #1037 from roramirez/lint-fix

Little lint fix
This commit is contained in:
Michael Teeuw
2017-09-30 13:36:38 +02:00
committed by GitHub