diff options
Diffstat (limited to 'dev/tools')
| -rw-r--r-- | dev/tools/coqdev.el | 2 | ||||
| -rwxr-xr-x[-rw-r--r--] | dev/tools/list-contributors.sh | 6 |
2 files changed, 4 insertions, 4 deletions
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el index 5f9f326750..d4f599484f 100644 --- a/dev/tools/coqdev.el +++ b/dev/tools/coqdev.el @@ -33,7 +33,7 @@ (defun coqdev-default-directory () "Return the Coq repository containing `default-directory'." - (let ((dir (locate-dominating-file default-directory "META.coq.in"))) + (let ((dir (locate-dominating-file default-directory "META.coq-core.in"))) (when dir (expand-file-name dir)))) (defun coqdev-setup-compile-command () 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 |