temporary Makefile leaked with new CMake configuration
By mistake, !986 (merged) contained a temporary Makefile
that should not be there.
Edited by Marco Clemencic
By mistake, !986 (merged) contained a temporary Makefile
that should not be there.