`(blog ,garaemon)

ポップカルチャーを摂取して、コードを吐き出す機械

2020-08-23から1日間の記事一覧

catkin profileが便利

catkin tools (catkinコマンド)を用いてソースコードをビルドする時に、ビルドオプションを変更したいことがあります。 たとえば、RelaseビルドとDebugビルドを切り替えたいときです。 このようなビルドオプションの切り替えには、catkin profileの機能が便…

find-name-diredから.gitディレクトリを除く

find-name-diredは, あるディレクトリ以下のファイルの文字列を一括で変換したりする際に、便利な関数です。 qiita.com www.gnu.org しかし, .gitディレクトリが候補に含まれてしまうと, 何かと不便なことが多いです。 以下のようにfind-name-argを変更する…