From 1b7565e81c52fd930d60c5a15679cdf18c8b9aa4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Jul 2020 09:21:59 +0200
Subject: Compatibility of make-change-log with MacOS X whose "sed" does not
 support "\+".

We make it compatible by expanding "[0-9]\+" into "[0-9][0-9]*".
---
 dev/tools/make-changelog.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/tools/make-changelog.sh b/dev/tools/make-changelog.sh
index de58527cca..413433ef41 100755
--- a/dev/tools/make-changelog.sh
+++ b/dev/tools/make-changelog.sh
@@ -28,7 +28,7 @@ esac
 printf "Fixes? (space separated list of bug numbers)\n"
 read -r fixes_list
 
-fixes_string="$(echo $fixes_list | sed 's/ /~  and /g; s,\([0-9]\+\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
+fixes_string="$(echo $fixes_list | sed 's/ /~  and /g; s,\([0-9][0-9]*\),`#\1 <https://github.com/coq/coq/issues/\1>`_,g' | tr '~' '\n')"
 if [ ! -z "$fixes_string" ]; then fixes_string="$(printf '\n  fixes %s,' "$fixes_string")"; fi
 
 # shellcheck disable=SC2016
-- 
cgit v1.2.3