DEV: patchbot: detect commit IDs starting with 7 chars

Some commit messages contain commit IDs as short as 7 chars, let's detect
them.

diff --git a/dev/patchbot/scripts/post-ai.sh b/dev/patchbot/scripts/post-ai.sh
index 3662fc85e978e236063fcef0658796d0226d4910..cfd21a00a41de71c5cf17cb1d84c90e8b6224c03 100755 (executable)
--- a/dev/patchbot/scripts/post-ai.sh
+++ b/dev/patchbot/scripts/post-ai.sh
@@ -380,7 +380,7 @@ for patch in "${PATCHES[@]}"; do
         resp=$(echo "$resp" | sed -e "s|#\([0-9]\{1,5\}\)|<a href='${ISSUES}\1'>#\1</a>|g")
 
         # put links to commit IDs
-        resp=$(echo "$resp" | sed -e "s|\([0-9a-f]\{8,40\}\)|<a href='${GITURL}\1'>\1</a>|g")
+        resp=$(echo "$resp" | sed -e "s|\([0-9a-f]\{7,40\}\)|<a href='${GITURL}\1'>\1</a>|g")
 
         echo -n "<TD nowrap align=center ${bkp[$cid]:+style='background-color:${BG_B}'}>$seq_num<BR/>"
         echo -n "<input type='radio' name='review' onclick='updt($seq_num,\"r\");' ${do_check:+checked} title='Start review here'/></TD>"