Remove the string-non-empty function which had no effect #1729
Merged
martin-cs merged 2 commits intodiffblue:developfrom Jan 14, 2018
Merged
Remove the string-non-empty function which had no effect #1729martin-cs merged 2 commits intodiffblue:developfrom
martin-cs merged 2 commits intodiffblue:developfrom
