build: prevent mixing catkin_make and catkin build on same build folder

[wjwwood]

There should be some sort of marker file in the build and devel spaces which prevents mixing the use of catkin_make, catkin_make_isolated, and catkin build on the same folders.

To be clear, it should prevent this:

$ ls
src
$ catkin_make
...
$ ls
src build devel
$ catkin build
Error: build space was created by caktin_make
       the usage of these two commands should not be mixed

[jbohren]

Such a marker should also prevent mixing catkin build and cakin build --merge-devel, right?

[wjwwood]

Yeah, that would be good also.

[jbohren]

This error checking has been implemented in #80. This should be good to close.