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