diff --git a/.github/workflows/build_docs.yml b/.github/workflows/build_docs.yml index f39991c2aac..41965ff6d1e 100644 --- a/.github/workflows/build_docs.yml +++ b/.github/workflows/build_docs.yml @@ -21,7 +21,6 @@ jobs: apt-get update apt-get install -y git git clone "https://token:${GITHUB_TOKEN}@github.com/${GITHUB_REPOSITORY}.git" . - git config --global --add safe.directory /__w/${GITHUB_REPOSITORY}/${GITHUB_REPOSITORY} shell: bash - name: Execute script to build our documentation and update pages diff --git a/docs/build_docs.sh b/docs/build_docs.sh index 22eb2ea6908..3800c4600e5 100755 --- a/docs/build_docs.sh +++ b/docs/build_docs.sh @@ -22,8 +22,10 @@ apt-get update apt-get -y install git rsync python3-pip python3-git python3-stemmer python3-virtualenv python3-setuptools python3 -m pip install -U sphinx==4.1.1 myst-parser==0.15.2 pygments==2.10.0 sphinx-rtd-theme==0.5.2 -export SOURCE_DATE_EPOCH=$(git log -1 --pretty=%ct) export REPO_NAME="${GITHUB_REPOSITORY##*/}" + +git config --global --add safe.directory /__w/${REPO_NAME}/${REPO_NAME} +export SOURCE_DATE_EPOCH=$(git log -1 --pretty=%ct) temp_docs_root=`mktemp -d` ls