Ask Your Question
0

how to change my source directory

asked 2013-11-12 08:50:33 -0500

Jessica gravatar image

updated 2013-11-14 12:31:33 -0500

tfoote gravatar image

I just changed my username and name of my home directory. Now I cannot use catkin_make because the source directory's name has been changed. How can I update, or change my source directory of catkin_ws?

edit retag flag offensive close merge delete

2 Answers

Sort by ยป oldest newest most voted
2

answered 2013-11-12 11:05:57 -0500

lindzey gravatar image

Have you tried removing catkin_ws/{build, devel} and running catkin_make again?

edit flag offensive delete link more
0

answered 2019-09-20 10:00:22 -0500

raushan gravatar image

Just run it and enjoy.

cd ~/catkin_ws/ && rm -r build devel && catkin_make
edit flag offensive delete link more

Your Answer

Please start posting anonymously - your entry will be published after you log in or create a new account.

Add Answer

Question Tools

Stats

Asked: 2013-11-12 08:50:33 -0500

Seen: 999 times

Last updated: Sep 20