"docs" space isn't deleted on `catkin clean` about catkin_tools_document HOT 4 CLOSED

That sounds great to me. There are potentially lots of places where catkin_tools could be extended externally, but adding those extension points as needed seems like a fine way to approach the issue. Specifically for adding spaces or adding a doc space, I can't think of any issues with doing that off-hand.

However, I'd suggest using doc as the folder name and refer to it as the doc space, since all of the other folder/spaces are singular already (except logs which I would have changed if I had noticed at the time).

+1 for adding spaces by extension.

from catkin_tools_document.

Interesting point on plural/singular. "Docs" does feel more natural do me, as would "tests" or "test_results" for a test verb. I think there is an internal kind of consistency in the way it is, in the sense that you do only have one build, and one install result, but each build produces many log files of output.

Either way, I'll mull over some thoughts about a new extension point, and maybe put up a PR at some point.

from catkin_tools_document.

This should be solved by catkin/catkin_tools#691 and #19

from catkin_tools_document.

Yup, thanks!

from catkin_tools_document.