diff --git a/dev/patchbot/scripts/post-ai.sh b/dev/patchbot/scripts/post-ai.sh index 654a6a161..8367912fa 100755 --- a/dev/patchbot/scripts/post-ai.sh +++ b/dev/patchbot/scripts/post-ai.sh @@ -404,7 +404,10 @@ for patch in "${PATCHES[@]}"; do echo -n "$seq_num
" echo -n "" - echo -n "$cid${date:+
$date}" + # only the first 8 chars of the commit id are displayed (enough to be + # unambiguous on one page); everything keyed (href, name=, cid[]) + # carries the full id produced by the pipeline, whatever its length. + echo -n "${cid:0:8}${date:+
$date}" echo -n "${pnum:+$pnum }$subj${author:+
$author
}" echo -n "" echo -n ""