WhatsTheTimeMrWolf

nicolaw 30th May 2018 at 3:44pm
Bash perf time
#!/usr/bin/env bash

# Wrap ourselves in a cosy time blanket.
if [[ "$(ps -o comm= $PPID)" != "time" ]]; then
  exec command time "$BASH" "$0" "$@"
fi

https://zachholman.com/talk/utc-is-enough-for-everyone-right