mirror of
https://github.com/github/gitignore.git
synced 2024-12-28 10:15:08 +08:00
Added ignore for files created by catkin_make_isolated
Simply execute `catkin_make_isolated` and `build` and `devel` will have different names, but should be ignored as well.
This commit is contained in:
parent
22a5eb3da7
commit
4162c93865
@ -13,6 +13,8 @@ msg/*Feedback.msg
|
|||||||
msg/*Goal.msg
|
msg/*Goal.msg
|
||||||
msg/*Result.msg
|
msg/*Result.msg
|
||||||
msg/_*.py
|
msg/_*.py
|
||||||
|
build_isolated/
|
||||||
|
devel_isolated/
|
||||||
|
|
||||||
# Generated by dynamic reconfigure
|
# Generated by dynamic reconfigure
|
||||||
*.cfgc
|
*.cfgc
|
||||||
|
Loading…
Reference in New Issue
Block a user