.github: use full GITHUB_REF path as target directories

This avoids conflicts for pull request builds.

Signed-off-by: Octavian Purdila <tavi@cs.pub.ro>

Author: tavip

.github/workflows/main.yml

@@ -29,14 +29,13 @@ jobs:
         run: |
           set -x
           env
-          export PUB_PATH=$(basename $GITHUB_REF)
           git clone --depth=1 git@github.com:linux-kernel-labs/linux-kernel-labs.github.io.git
           cd linux-kernel-labs.github.io
-          rm -rf $PUB_PATH
-          mkdir -p $PUB_PATH
-          cp -r ../Documentation/output/teaching/* $PUB_PATH/
+          rm -rf $GITHUB_REF
+          mkdir -p $GITHUB_REF
+          cp -r ../Documentation/output/teaching/* $GITHUB_REF
           git config --global user.email "github.actions@linux-kernel-labs.gihub.io"
           git config --global user.name "GitHub Actions"
-          git add $PUB_PATH
-          git commit --allow-empty -m "Publish $PUB_PATH (built from linux-kernel-labs/linux/$GITHUB_REF)"
+          git add $GITHUB_REF
+          git commit --allow-empty -m "Publish $GITHUB_REF"
           git push