Ask Your Question
0

how to change my source directory

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

Jessica gravatar image

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

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 -0600

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 -0600

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 -0600

Seen: 1,057 times

Last updated: Sep 20