mirror of
https://github.com/github/gitignore.git
synced 2026-04-02 07:47:42 +00:00
Simply execute `catkin_make_isolated` and `build` and `devel` will have different names, but should be ignored as well.
52 lines
538 B
Plaintext
52 lines
538 B
Plaintext