Published May 10, 2020
Here's a simple Python script to pretty-print a JSON file:
#!/usr/bin/env python
from __future__ import print_function
import sys
import json
try:
json.dump(json.load(sys.stdin), sys.stdout, sort_keys=True, indent=4)
except ValueError as err:
print("Error:", err, file=sys.stderr)
exit(1)
To format JSON from the pasteboard:
To format JSON in a file:
Both with print the formatted JSON to stdout. To write to a file, you can redirect the output like this:
$ ppjson < input_filename > output_filename
Or, you could format JSON from the pasteboard (using pbpaste
piped through ppjson
) the copy the formatted JSON back to the pasteboard (using pbcopy
):
$ pbpaste | ppjson | pbcopy
Published May 10, 2020
I can never remember the commands to delete a Git tag. It's one of those things I don't do frequently enough to remember — I always have to look it up.
To delete a local tag called TAGNAME
:
$ git tag --delete TAGNAME
To delete a remote tag called TAGNAME
:
$ git push --delete origin TAGNAME
But rather than have to enter in two commands, I wrote a script that combines them:
#!/usr/bin/env bash
set -euo pipefail
E_BADARGS=85
if [ $# -ne 1 ]; then
echo "Usage: $(basename $0) tag-name"
exit $E_BADARGS
fi
tagname="$1"
# Delete the local tag
echo "Deleting local tag $tagname"
git tag --delete $tagname
# Delete the remote tag
echo "Deleting remote tag $tagname"
git push --delete origin $tagname
That script is saved in my ~/bin
directory under the name git-rmtag
. Using that naming convention, you can run it like this:
and it will delete the local and remote tags.
Published May 10, 2020
It has been over five years since I have actively updated my blog. I have done some recent work that I wanted to post about, so I have decided to reboot my blog.
I have removed the old posts that I had up here previously. Most posts were badly outdated. I will repost some of the topics that are still relevant.