diff options
author | Teddy Wing | 2018-04-19 00:35:10 +0200 |
---|---|---|
committer | Teddy Wing | 2018-04-19 00:35:10 +0200 |
commit | 5670759a5623fa4cef6cb0d37602bb41b7c34c5c (patch) | |
tree | 4c5ad675f6784932c366480f778b2c285925a24f | |
parent | c1d64dc4e0a1328107c05bb952133c0ca70b6e1c (diff) | |
download | redprine-5670759a5623fa4cef6cb0d37602bb41b7c34c5c.tar.bz2 |
extract_data_from_pull_request_json(): Use real GitHub username
Get the username from the command line argument-loaded variable instead
of my hard-coded username.
-rwxr-xr-x | redprine | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -82,7 +82,7 @@ function extract_data_from_pull_request_json () { created_at }) | map( - select(.user == "teddywing") + select(.user == '"$GITHUB_USERNAME"') )' } |