[TRAVIS] fix DEVEL_BUILD#157
Merged
KrisThielemans merged 10 commits intomasterfrom travis_gcc6Dec 9, 2018
+34-17
Commits
Commits on Dec 4, 2018
- committedKris Thielemans
- committedKris Thielemans
Commits on Dec 6, 2018
- authored
- authored
Commits on Dec 8, 2018
- committedKris Thielemans
- committedKris Thielemans
- committedKris Thielemans
- committedKris Thielemans
- committedKris Thielemans
- committedKris Thielemans