From 904e09267549879e90e7a8a9b7138bbe5d5ba368 Mon Sep 17 00:00:00 2001
From: Hari Sekhon <harisekhon@gmail.com>
Date: Fri, 2 Oct 2020 15:49:52 +0100
Subject: [PATCH] updated github_delete_ssh_public_keys.sh

---
 github_delete_ssh_public_keys.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/github_delete_ssh_public_keys.sh b/github_delete_ssh_public_keys.sh
index d1410db0..05468c7f 100755
--- a/github_delete_ssh_public_keys.sh
+++ b/github_delete_ssh_public_keys.sh
@@ -52,7 +52,7 @@ min_args 1 "$@"
 
 filter="$1"
 
-timestamp "Getting SSH public keys" >&2
+timestamp "Getting SSH public keys"
 "$srcdir/github_api.sh" "/user/keys" |
 jq -r '.[] | [.id, .title] | @tsv' |
 while read -r key_id title; do