bits release in progress

Misc shell tricks

Tags shell

remote diff

diff over SSH:

ssh host 'cat path/to/file' | diff -u - local/file | cdiff

Remove leading characters

For a string representing a number, which could be prefixed by one or more 0, we want to remove all the leading 0 (i.e.: 00090800 should become 90800):

$ U=00090800
$ echo $((${U#${U%?${U#*[!0]}}}+0))

$ U=aaaafoobar
$ echo ${U#${U%?${U#*[!a]}}}

Shells compatible (bash, ash, dash, fbsd, ...), twice as fast as a loop trimming and two order of magnitude faster than any solution requiring to execute a command and/or a pipe (bc, sed, etc.).

Duplicate stderr for logging

The bash4 way:

ERR { tee stderr.log; } 1>&2
exec 2>&${ERR[1]}
# the script, like :
date kjuio

More compatible way:

mkfifo /tmp/fifo
tee /dev/tty 0< /tmp/fifo 1>&2 &
exec 2> /tmp/fifo
rm -f /tmp/fifo
# the script
echo "to stderr" 1>&2
echo "to stdout"
exec 2>&-

Another common way:

exec > >(tee stdout.log) 2> >(tee stderr.log >&2)
# the script