Mon, 15 Jul 2024 13:22:56 -0500
Fix for no-nerdfonts experience
969 | 1 | warn() { echo "$*" >&2; } |
2 | die() { warn "$*"; exit 1; } | |
3 | ||
4 | clone_or_pull() { | |
5 | if ! [ -d $2 ]; then | |
6 | git clone --single-branch --depth 1 "$1" $2 | |
7 | else | |
8 | echo "$2:" | |
9 | git -C "$2" pull | |
10 | fi | |
11 | } |