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