push_to_space.sh: auto-inject HF_TOKEN into push URL when set

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

server/space/push_to_space.sh

@@ -6,14 +6,19 @@
 # Prereq once:
 #   git remote add space https://huggingface.co/spaces/lanczos/graphtestbed
 #
-# When git prompts for credentials on push:
-#   user     = lanczos
-#   password = $HF_TOKEN
+# Auth: export HF_TOKEN before running and the script will inject it into
+# the push URL; otherwise git will prompt for username/password
+# (user = lanczos, password = the token).
 set -euo pipefail
 
 BRANCH=$(git rev-parse --abbrev-ref HEAD)
 TEMP="space-deploy-$(date +%s)"
 
+PUSH_TARGET="space"
+if [[ -n "${HF_TOKEN:-}" ]]; then
+  PUSH_TARGET="https://lanczos:${HF_TOKEN}@huggingface.co/spaces/lanczos/graphtestbed"
+fi
+
 trap 'git checkout "$BRANCH" >/dev/null 2>&1 || true; \
       git branch -D "$TEMP" >/dev/null 2>&1 || true' EXIT
 
@@ -24,7 +29,7 @@ cp server/space/README.md README.md
 cp server/space/Dockerfile Dockerfile
 git add README.md Dockerfile
 git commit --no-verify -m "deploy: overlay server/space/{README,Dockerfile} at root"
-git push -f space "$TEMP:main"
+git push -f "$PUSH_TARGET" "$TEMP:main"
 echo
 echo "pushed to space/main"
 echo "URL: https://lanczos-graphtestbed.hf.space/"