Cleanup and extend user-directed output#2184
Merged
tautschnig merged 10 commits intodiffblue:developfrom Jun 5, 2018
Merged
Commits
Commits on Jun 4, 2018
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed