#!/bin/sh
# The git credential helper of the workspace repositories (#422).
#
# The executor sets it in the local config of each project repository,
# for the host of that repository only. It gives the GH_TOKEN of the
# environment, so `git push` in run_with_secret works with the token of
# that command. The token is never in a file or in the git config.
# With no GH_TOKEN, it gives nothing.
cat > /dev/null
if [ "$1" = get ] && [ -n "$GH_TOKEN" ]; then
  printf 'username=x-access-token\npassword=%s\n' "$GH_TOKEN"
fi
