Fix list-constributors.sh script.

1 files changed, 3 insertions, 3 deletions

diff --git a/dev/tools/list-contributors.sh b/dev/tools/list-contributors.sh
index c968f2e952..0b0d01c7e2 100644..100755
--- a/dev/tools/list-contributors.sh
+++ b/dev/tools/list-contributors.sh
@@ -1,15 +1,15 @@
 #!/usr/bin/env bash
 # For compat with OSX which has a non-gnu sed which doesn't support -z
-SED=`which gsed || which sed`
+SED=`(which gsed || which sed) 2> /dev/null`
 
 if [ $# != 1 ]; then
-  error "usage: $0 rev0..rev1"
+  echo "usage: $0 rev0..rev1"
   exit 1
 fi
 
 git shortlog -s -n --group=author --group=trailer:Co-authored-by $1 | cut -f2 | sort -k 2 | grep -v -e "coqbot" -e "^$" > contributors.tmp
 
 cat contributors.tmp | wc -l | xargs echo "Contributors:"
-cat contributors.tmp | gsed -z "s/\n/, /g"
+cat contributors.tmp | $SED -z "s/\n/, /g"
 echo
 rm contributors.tmp