rename port to omp-pygienium (repo renamed)
Some checks failed
port-to-omp / port (push) Failing after 5s

This commit is contained in:
2026-08-10 15:18:01 -04:00
parent f6f997bb21
commit be76b31a6e
2 changed files with 5 additions and 5 deletions

View File

@@ -1,7 +1,7 @@
name: port-to-omp
# Regenerate the omp port of pygenium from this repo and push it to
# Mike/omp-pygenium.
# Mike/omp-pygienium.
#
# Prerequisites on git.freno.me:
# - an access token with write:repository scope, stored as the repo/org
@@ -29,7 +29,7 @@ jobs:
- name: Port to omp
env:
GITEA_TOKEN: ${{ secrets.GITEA_TOKEN }}
OMP_REPO: omp-pygenium
OMP_REPO: omp-pygienium
run: |
set -euo pipefail
URL="https://oauth2:${GITEA_TOKEN}@git.freno.me/Mike/${OMP_REPO}.git"