diff --git a/misc/wget-pr.sh b/misc/wget-pr.sh new file mode 100755 index 000000000..d91b172e7 --- /dev/null +++ b/misc/wget-pr.sh @@ -0,0 +1,9 @@ +#!/bin/sh + +if [ $# -ne "1" ]; then + echo "usage: $0 " + exit 1 +fi + +pr=$1 +wget https://github.com/namhyung/uftrace/pull/$pr.patch