Re #970. Naughty quick fix of CMakeLists directly on develop.

Somehow it had picked up some entries that don't yet exist in
this directory. Doing it this way avoids any git merging cleverness
- but watch out to make sure it doesn't happen again.