specify user before merging

parent e0d67c0a
Pipeline #14266 passed with stages
in 1 minute and 20 seconds
......@@ -83,5 +83,5 @@ merge into local:
- master@solidstate/lectures
- git checkout local
- git merge master
- git diff-index --quiet master || git -c "user.name=$GITLAB_USER_NAME" -c "user.email=$GITLAB_USER_EMAIL" merge master
- "git push https://$GITLAB_PUSH_KEY@gitlab.kwant-project.org/solidstate/lectures.git local"
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment