pin: fix HASH replacement; full sha in URL, short hash for display

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

.forgejo/workflows/pin.yaml

@@ -62,8 +62,7 @@ jobs:
                         git remote add origin https://git.ziemlichoptimal.de/niels/randomp2p.git
                         git fetch --depth 1 origin ${SHA}
                         git checkout FETCH_HEAD
-                        SHORT="$(echo "${SHA}" | cut -c1-8)"
-                        sed -i "s/HASH/${SHORT}/g" /work/repo/index.html
+                        sed -i "s#commit/HASH#commit/${SHA}#; s#>HASH<#>$(echo "${SHA}" | cut -c1-8)<#" /work/repo/index.html
                         rm -rf /work/repo/.git
                     volumeMounts:
                       - { name: work, mountPath: /work }