Cleaning up more files on make clean_all.
Authored by: debug 2018-09-25
Parent: [r5981]
Child: [r5983]