correct key name
Some checks failed
port-to-omp / port (push) Failing after 4s

This commit is contained in:
2026-08-11 08:58:35 -04:00
parent 8768f9de97
commit 6ceb3c4889

View File

@@ -1,6 +1,6 @@
name: port-to-omp
# Regenerate the omp port of pygenium from this repo and push it to
# Regenerate the omp port of pygienium from this repo and push it to
# Mike/omp-pygienium.
#
# Prerequisites on git.freno.me:
@@ -28,14 +28,14 @@ jobs:
- name: Port to omp
env:
PORTING_TOKEN: ${{ secrets.PORTING_TOKEN }}
PORTING_KEY: ${{ secrets.PORTING_KEY }}
OMP_REPO: omp-pygienium
run: |
set -euo pipefail
# Trim the secret: a stray newline from pasting silently breaks
# oauth2 basic-auth. Fail loudly when it is missing entirely.
: "${PORTING_TOKEN:?PORTING_TOKEN secret is not set}" || exit 1
PORTING_TOKEN="$(printf '%s' "${PORTING_TOKEN}" | tr -d '[:space:]')"
: "${PORTING_TOKEN:?PORTING_TOKEN secret is not set}"
URL="https://oauth2:${PORTING_TOKEN}@git.freno.me/Mike/${OMP_REPO}.git"
# The omp checkout lives in $RUNNER_TEMP, outside the pi checkout:
# the port script refuses to write into a subdirectory of its own