diff --git a/.gitea/workflows/convert-html-docs.yaml b/.gitea/workflows/convert-html-docs.yaml
index fd6e268fe..628e96d6d 100644
--- a/.gitea/workflows/convert-html-docs.yaml
+++ b/.gitea/workflows/convert-html-docs.yaml
@@ -163,22 +163,24 @@ jobs:
REPO=$(jq -r .repository.full_name "$GT_EVENT_PATH")
OWNER=$(echo "$REPO" | cut -d'/' -f1)
REPO_NAME=$(echo "$REPO" | cut -d'/' -f2)
- echo "Gitea REPO: $REPO_NAME"
- echo "Gitea PR Number: $PR_NUMBER"
- echo "Gitea Owner: $OWNER"
+ echo "REPO=$REPO" >> $GITHUB_ENV
+ echo "REPO_NAME=$REPO_NAME" >> $GITHUB_ENV
+ echo "PR_NUMBER=$PR_NUMBER" >> $GITHUB_ENV
+ echo "OWNER=$OWNER" >> $GITHUB_ENV
# exit 1
- name: List changed files in PR
id: changed_files
run: |
- PR_NUMBER=$(jq -r .pull_request.number "$GT_EVENT_PATH")
- REPO=$(jq -r .repository.full_name "$GT_EVENT_PATH")
+ # PR_NUMBER=$(jq -r .pull_request.number "$GT_EVENT_PATH")
+ # REPO=$(jq -r .repository.full_name "$GT_EVENT_PATH")
echo "PR #$PR_NUMBER from repo $REPO"
# Extract owner and repo name
- OWNER=$(echo "$REPO" | cut -d'/' -f1)
- REPO_NAME=$(echo "$REPO" | cut -d'/' -f2)
+ # OWNER=$(echo "$REPO" | cut -d'/' -f1)
+ # REPO_NAME=$(echo "$REPO" | cut -d'/' -f2)
+ echo "Repository $REPO_NAME in organization $OWNER"
# Use Gitea API to get changed files
# Requires an API token with repo read access