diff --git a/.catkin_workspace b/.catkin_workspace new file mode 100644 index 0000000..52fd97e --- /dev/null +++ b/.catkin_workspace @@ -0,0 +1 @@ +# This file currently only serves to mark the location of a catkin workspace for tool integration