bin/git-set-head (htmlized)

Warning: this is an htmlized version!
The original is here, and
the conversion rules are here.

#!/bin/sh
# (find-es "git")
# (find-es "git" "detached-head")
# (find-man "1 git-checkout")

# (find-gitsrcfile "builtin/checkout.c")
# (find-gitsrcgrep "grep -nH -e 'detached HEAD' $(cat .files)")
# (find-gitsrcgrep "grep -nH -e 'detach_advice' $(cat .files)")
# (find-gitsrcfile "advice.c" "detach_advice")

set +v
#  git checkout $(git rev-list -n 1 HEAD)
git checkout -q $(git rev-list -n 1 HEAD)
git reset --soft $1