Wednesday, March 10, 2010

git rename branch

and here's how to rename a branch

git branch -m

git push automatic

i was tired of typing git push origin , so I finally deciphered how to configure the deafault remote and branch to merge

git config --global branch.mylocalbranchname.remote origin
git config --global branch.mylocalbranchname.merge mylocalbranchname


my remote branch and local branch have the same name, i don't know yet how to configure it having different name ; ) somebody ?

linux find exclude dir grep

using linux, here is a way to find all files with a given extension, with a given content, within a directory excluding a particular path

find -name "*.extension" ! -path './excluded_dir/*' -exec grep "searched_content" {} --color -H \;


it took me a little while to construct, so i find it cool to save it here

cancel script completely on ctrl-c

I found this question interesting: basically how to cancel completely a script and all child processes : You do this by creating a subro...