rm--

  man -T bash bash | ps2pdf - bash.pdf

first bash is the page you are looking for

rm--

pip install natsort
import os

src_dir = '/tmp/in'
dst_dir = '/tmp/out'
starting_nb = 11  # new filename starting with this number
[os.rename(src_dir + os.sep + f,dst_dir + os.sep + str(i) + '.' + f.split('.')[1]) for (i,f) in enumerate(natsort.natsorted(os.listdir(src_dir)),starting_nb)]

rm--

Deleting is also a pretty simple task (despite it feeling a bit kludgy):

git push origin :newfeature

That will delete the newfeature branch on the origin remote, but you’ll still need to delete the branch locally with git branch -d newfeature.

http://gitready.com/beginner/2009/02/02/push-and-delete-branches.html

rm--

merged_branches(){
  local red=`tput setaf 1`
  local green=`tput setaf 2`
  local bold=`tput bold`
  local reset=`tput sgr0`

  local current_branch=$(git rev-parse --abbrev-ref HEAD)
  for branch in $(git branch --merged | cut -c3-)
    do
      if [[ $branch = $current_branch ]]; then

rm--

cat ~/.zsh_history | awk -F\; '{ print $2 }' | sort | uniq -c | sort -n

rm--

osx

git mergetool -t opendiff

ubuntu linux

git mergetool -t meld

rm--

# delete unused remote branches
git remote prune origin

rm--

git stash show -p stash@{0}

rm--

# debug salt states:

`sudo salt-call state.sls <your-salt-state-to-debug> test=True`

rm--

{
    "url": "http://example.com/api/23/",
    "author": 1,
    "date_created": "2015-03-26T11:01:23.262391Z",
    "date_updated": "2015-03-26T11:01:23.262391Z",
    "html": "<form></form>",
    "javascript": "<script></script>",
    "form": {
        "id": 123,
        "method": "POST",